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

Update WP cache

parent 92cb4e90
No related branches found
No related tags found
No related merge requests found
Showing
with 65 additions and 0 deletions
[kernel] Parsing lhost.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta] Successful translation
/* Generated by Frama-C */
struct S {
unsigned int owner ;
int data ;
};
extern unsigned int current_id;
int read(struct S *s)
{
int __retres;
/*@ assert
only_owner_reads: meta:
¬\separated(&s->data, &s->owner) ⇒ s->owner ≡ current_id;
*/
if (s->owner != current_id) {
__retres = -1;
goto return_label;
}
/*@ assert only_owner_reads: meta: s->owner ≡ current_id; */
__retres = s->data;
return_label: return __retres;
}
int write(struct S *s, int val)
{
int __retres;
/*@ assert
only_owner_reads: meta:
¬\separated(&s->data, &s->owner) ⇒ s->owner ≡ current_id;
*/
if (s->owner != current_id) {
__retres = -1;
goto return_label;
}
/*@ assert only_owner_writes: meta: s->owner ≡ current_id; */
s->data = val;
__retres = 0;
return_label: return __retres;
}
/*@ meta "only_owner_reads"; */
/*@ meta "only_owner_writes";
*/
{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0042,
"steps": 20 }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0127,
"steps": 157 }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0092,
"steps": 158 }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0129,
"steps": 47 }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.005,
"steps": 29 }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.008,
"steps": 20 }
{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
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