source: CIVL/examples/languageFeatures/pointerAddBad6.c@ afc300c

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

Merged Ziqing's Short-circuit branch into trunk.

The branch generally did 3 changes:

  1. Let transition carries a clause which will be added to the PC instead of the new PC
  2. Transform short-circuit away by adding a transformer and a error side-effect free evaluator. The evaluator will be used to evaluate expressions in the context like guard or quantified expressions
  3. The evaluation of LOP, LAND and LIMPLIES are now intuitive.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@4166 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 159 bytes
RevLine 
[8777216]1#include <civlc.cvh>
[eeed32c]2
[8777216]3$input int offset;
4$assume(0<=offset && offset<=1);
[7c73e9d]5int main() {
[8777216]6 int a = 8;
7 void *p = &a + 1;
[7c73e9d]8 void *q = p + offset;
[4c67e83]9
10 return 0;
11}
Note: See TracBrowser for help on using the repository browser.