source: CIVL/examples/compare/adder/adder_spec.cvl@ a6d2043

1.23 2.0 main test-branch
Last change on this file since a6d2043 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: 879 bytes
Line 
1#include <civlc.cvh>
2/*****************************************
3 * SOURCE: adder_spec.c by vsl@udel
4 * The source program is included in FEVS
5 * vsl.cis.udel.edu/fevs
6 * FILE: adder_spec.cvl
7 * DESCRIPTION: This a manually translated
8 * CIVL program which is based on "adder_spec.c"
9 * This program sums all elements of an array
10 * up.
11 *
12 * AUTHOR: Ziqing Luo
13 * COMMANS: civl verify adder_spec.cvl
14 * -inputNB=10
15 * or
16 * make civl_spec
17 *****************************************/
18
19#include<stdio.h>
20$input int NPROCS; /* useless input variables for civl compare */
21$input int NPROCSB;
22$input int N;
23$input int NB;
24$input double a[N];
25$output double SUM;
26$assume(0 < N && N < NB);
27
28void main() {
29 double result = 0.0;
30 int n = N;
31 int i;
32
33 for (i=0; i<n; i++) result += a[i];
34 SUM = result;
35 printf("%lf\n",result);
36}
Note: See TracBrowser for help on using the repository browser.