source: CIVL/examples/languageFeatures/pointersBad.cvl@ 050ee5d

1.23 2.0 main test-branch
Last change on this file since 050ee5d was 050ee5d, checked in by Ziqing Luo <ziqing@…>, 11 years ago

covers more

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@2371 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 474 bytes
RevLine 
[262ecde]1/* Commandline execution:
2 * civl verify pointersBad.cvl
3 * */
4#include<civlc.cvh>
5#include<stdlib.h>
6
7$output int out;
[f79e288]8$input int x;
[050ee5d]9$input int *x_ptr;
[262ecde]10void main() {
11 int a;
[f79e288]12 int* b, *c;
13 int * nilPtr = NULL;
[262ecde]14
[f79e288]15 c = (void *)(-1);
[262ecde]16 b = (int *)malloc(sizeof(int));
17 free(b);
18 a = *(&out);
[f79e288]19 $choose {
[050ee5d]20 $when(x == 2) {a = *x_ptr;}
21 $when(x == 1) {c = &a + 1; a = *c;}
[f79e288]22 $when(x == 0) {a = *c;}
[050ee5d]23 $when(x >=3 ) {a = *b;}
[f79e288]24 $when(x < 0 ) {a = *nilPtr;}
25 }
[262ecde]26}
Note: See TracBrowser for help on using the repository browser.