← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/jessie/weber2.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/weber2.c
 
1
 
 
2
/*@
 
3
requires last > first;
 
4
requires \valid_range(first, 0, last-first-1);
 
5
ensures *\result == value;
 
6
*/
 
7
int* find_int_array (int* first, int* last, int value ) {}
 
8
 
 
9
void f() {
 
10
  int *i, *j, k, *l;
 
11
  l = find_int_array(i,j,k);
 
12
}
 
13
 
 
14
/*
 
15
Local Variables:
 
16
compile-command: "LC_ALL=C make -j weber2"
 
17
End:
 
18
*/