source: CIVL/examples/library/civlc/translate_ptr.cvl@ 7dbb0db

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since 7dbb0db was 3ff27cf, checked in by Manchun Zheng <zmanchun@…>, 11 years ago

updated examples since $assert/$assume has been changed to functions; fixed the model builder for the new side-effect remover.

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

  • Property mode set to 100644
File size: 801 bytes
Line 
1/*
2* This example demonstrates the usage of the civl system function:
3* void * $translate_ptr(void *ptr, void *obj);
4* Command line execution:
5* civl verify translate_ptr.cvl
6*/
7
8#include<civlc.cvh>
9#include<pointer.cvh>
10
11typedef struct node{
12 int x;
13 int y;
14} node;
15
16typedef struct point{
17 double a;
18 double b;
19}point;
20
21void main(){
22 int *q;
23 double *p;
24 node *list;
25 point set[5];
26 point t;
27 double a[3][3][3];
28 int b[3][3];
29 double (*p1)[] = &a[1][2]; // p has type pointer-to-array-of-double
30
31 q = (int*)$translate_ptr(p1, &b);
32 $assert((q == &b[1][2]));
33 list = (node*)$malloc($here, sizeof(node)*5);
34 q = & (list+2)->y;
35 p = (double*)$translate_ptr(q, &t);
36 $assert((p == &t.b));
37 p = & t.a;
38 q = (int*)$translate_ptr(p, list);
39 $assert((q == &list->x));
40 $free(list);
41}
Note: See TracBrowser for help on using the repository browser.