source: CIVL/mods/dev.civl.abc/examples/preproc/dotdot_preproc.txt

main
Last change on this file was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 686 bytes
RevLine 
[c510c2d]1#include<assert.h>
2
3int main() {
4 int m = 0;
5 int n = 10;
6 int k = n-1;
7 int a[n];
8
9 for (int i = 0; i < n; i++)
[aad342c]10 a[i] = i;
[c510c2d]11
12 $assert($forall (int j:0.. k) a[j]==0);
13 $assert($forall (int j:0..n-1) a[j]==0);
14 $assert($forall (int j:0.. n-1) a[j]==0);
15 $assert($forall (int j:0 .. n-1) a[j]==0);
16 $assert($forall (int j:0 ..n-1) a[j]==0);
17 $assert($forall (int j:0..(n-1)) a[j]==0);
18 $assert($forall (int j:m ..9) a[j]==0);
19 $assert($forall (int j:m +0..9) a[j]==0);
20 $assert($forall (int j:m -0..9) a[j]==0);
21 $assert($forall (int j:0..+9) a[j]==0);
22 $assert($forall (int j:0..-9+18) a[j]==0);
[aad342c]23 $assert($forall (double j: m ..k) a[j]==0);
24 $assert($forall (double j: m..k) a[j]==0);
25}
Note: See TracBrowser for help on using the repository browser.