Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
62a61e53
Commit
62a61e53
authored
Jun 19, 2020
by
Virgile Prevosto
Browse files
[tests] update oracles
parent
9c909bee
Changes
2
Hide whitespace changes
Inline
Side-by-side
tests/spec/oracle/assigns_array.res.oracle
View file @
62a61e53
...
...
@@ -36,8 +36,8 @@ int h(int reset, int n)
int i;
int r = 0;
i = 0;
/*@ for
bar
: loop assigns
\nothing
;
for
foo
: loop assigns
Tab[0 .. i]
; */
/*@ for
foo
: loop assigns
Tab[0 .. i]
;
for
bar
: loop assigns
\nothing
; */
while (i < n) {
r += Tab[i];
if (reset) Tab[i] = 0;
...
...
tests/spec/oracle/bts0578.res.oracle
View file @
62a61e53
...
...
@@ -7,11 +7,11 @@ void main(void)
int i;
int t[10];
i = 0;
/*@ loop invariant \true;
loop assigns t[0 .. i];
/*@ loop assigns t[0 .. i];
loop invariant \true;
for foo: loop assigns t[0 .. i];
for foo: loop invariant \true;
for foo: loop invariant \true;
for foo: loop assigns t[0 .. i];
loop variant 0;
*/
while (i < 10) {
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment