diff options
| author |  qadeer <unknown> | 2011-02-06 06:13:47 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2011-02-06 06:13:47 +0000 |
| commit | 3718f4836a0a5d80b07f2e9f41cacbebbf7958fe (patch) | |
| tree | 75799a4a9330f355e58f66a612e0cc7de646a769 /Test/stratifiedinline | |
| parent | 0f96c5cb02b4f1354841f22d29a7dbc86a12be51 (diff) | |
implemented /UseUnsatCoreForInlining option for use in stratified inlining
Diffstat (limited to 'Test/stratifiedinline')
| -rw-r--r-- | Test/stratifiedinline/bar7.bpl | 43 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar8.bpl | 42 |
2 files changed, 85 insertions, 0 deletions
diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl new file mode 100644 index 00000000..747510de --- /dev/null +++ b/Test/stratifiedinline/bar7.bpl @@ -0,0 +1,43 @@ +var i: int;
+var m: int;
+
+procedure {:inline 1} foo()
+modifies i;
+{
+ if (i < 80) {
+ i := i + 1;
+ call foo();
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m)
+ {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 1;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ if (*) {
+ call foo();
+ } else {
+ call bar1(0);
+ call bar2(0);
+ }
+ assert i < 10;
+}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl new file mode 100644 index 00000000..d447e3a7 --- /dev/null +++ b/Test/stratifiedinline/bar8.bpl @@ -0,0 +1,42 @@ +var i: int;
+var m: int;
+
+procedure {:inline 1} foo()
+modifies i;
+{
+ if (i < 80) {
+ i := i + 1;
+ call foo();
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m) {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 2;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ if (*) {
+ call foo();
+ } else {
+ call bar1(0);
+ call bar2(0);
+ }
+ assert i < 10;
+}
\ No newline at end of file |