← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to tests/jessie/annot_assert.c

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
tests/jessie/annot_assert.c
 
1
 
 
2
//#pragma AnnotationPolicy(WeakPre)
 
3
//#pragma AbstractDomain(Box)
 
4
#pragma CheckArithOverflow(yes)
 
5
 
 
6
int f(int i) {
 
7
  //@ assert (i > 0);
 
8
  return i;
 
9
}
 
10
 
 
11
int ff(int i) {
 
12
  int j = 1;
 
13
  //@ assert (i+j > 0);
 
14
  return i;
 
15
}
 
16
 
 
17
/* 
 
18
Local Variables:
 
19
compile-command: "PPCHOME=../.. LC_ALL=C make annot_assert"
 
20
End:
 
21
*/