source: CIVL/include/impls/int_div_no_checking.cvl@ 4e993a9

main test-branch
Last change on this file since 4e993a9 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

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

  • Property mode set to 100644
File size: 810 bytes
Line 
1#ifndef _INT_DIV_CIVL_
2#define _INT_DIV_CIVL_
3
4$system[civlc] void $assume(_Bool expr);
5
6int $int_div(int numerator, int denominator) {
7 if (numerator == 0)
8 return 0;
9 if (numerator >= 0) {
10 if (denominator >= 0)
11 return numerator/denominator;
12 else
13 return -(numerator/(-denominator));
14 } else {
15 if (denominator >= 0)
16 return -((-numerator)/denominator);
17 else
18 return (-numerator)/(-denominator);
19 }
20}
21
22int $int_mod(int numerator, int denominator) {
23 if (numerator == 0)
24 return 0;
25 if (numerator >= 0) {
26 if (denominator >= 0)
27 return numerator%denominator;
28 else
29 return numerator%(-denominator);
30 } else {
31 if (denominator >= 0)
32 return -((-numerator)%denominator);
33 else
34 return -((-numerator)%(-denominator));
35 }
36}
37
38#endif
Note: See TracBrowser for help on using the repository browser.