src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c · f7a1cd74ac80ee7bd1df9bd9bf44b2e83097c271 · pub / frama-c

12 years ago

[E-ACSL] handle specified function without code. BTW that fixes bugs #1300 and #1340. · f7a1cd74

Julien Signoles authored 12 years ago

[E-ACSL] convert postcondition even in presence of untranslated assigns clause
[E-ACSL] fix bug when the translation of a predicate containing \at is abruptely stopped because of a not-yet-implemented construct (the generated code contained undeclared __e_acsl_at variables)

f7a1cd74

History

[E-ACSL] handle specified function without code. BTW that fixes bugs #1300 and #1340.

Julien Signoles authored 12 years ago

[E-ACSL] convert postcondition even in presence of untranslated assigns clause
[E-ACSL] fix bug when the translation of a predicate containing \at is abruptely stopped because of a not-yet-implemented construct (the generated code contained undeclared __e_acsl_at variables)