Skip to content
Snippets Groups Projects
Commit 2a122822 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

update oracles

parent a029191d
No related branches found
No related tags found
No related merge requests found
[kernel] Parsing cxx_c_link.cpp (external front-end)
Now output intermediate result
[kernel] Parsing cxx_c_link.c (with preprocessing)
/* Generated by Frama-C */
#include "__fc_alloc_axiomatic.h"
/*@
axiomatic dynamic_allocation {
predicate is_allocable{L}(ℤ n)
reads __fc_heap_status;
axiom never_allocable{L}:
∀ ℤ i; i < 0 ∨ i > 18446744073709551615UL ⇒ ¬is_allocable(i);
}
*/
[kernel] Parsing ghost_extern_c.cpp (external front-end)
Now output intermediate result
/* Generated by Frama-C */
/*@ ghost int _Z7ghost_x; */
/*@ ghost int ghost_x; */
int real_x;
/*@ lemma sync{L}: _Z7ghost_x ≡ real_x;
/*@ lemma sync{L}: ghost_x ≡ real_x;
*/
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment