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