Skip to content
Snippets Groups Projects
Commit c55b7842 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Test that RefUsage takes lemmas in account

parent 4e275860
No related branches found
No related tags found
No related merge requests found
# frama-c -wp [...]
[kernel] Parsing tests/wp_usage/ref-usage-lemmas.i (no preprocessing)
[wp] Running WP plugin...
.................................................
... Ref Usage
.................................................
Init: { &a b }
Function foo: { &a b *x }
Function main: { &a b __retres }
.................................................
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
------------------------------------------------------------
Goal Pre-condition (file tests/wp_usage/ref-usage-lemmas.i, line 30) in 'main':
Prove: true.
------------------------------------------------------------
/* run.config
OPT: -wp-msg-key refusage
*/
/* run.config_qualif
DONTRUN:
*/
int a ;
int b ;
/*@ axiomatic A{
logic int* get reads \nothing ;
logic int* get_h = &a ;
axiom a: get_h == get ;
}
*/
/*@ axiomatic B{
logic integer value reads \nothing ;
axiom b: value == b ;
}
*/
void foo(int* x){
*x = a = b ;
}
/*@ requires a <= b ; */
int main(void){
int e ;
foo(&e) ;
}
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