Skip to content
Snippets Groups Projects
Commit 4c6abaa6 authored by Forget Julien's avatar Forget Julien
Browse files

Merge branch 'master' of gitlab.cristal.univ-lille.fr:otawa-plugins/WSymb

parents a98a94fb 74d6af08
Branches
No related tags found
No related merge requests found
......@@ -389,6 +389,8 @@ void writePWF(formula_t *f, FILE *out, long long *bounds) {
writePWF(f->children + i, out, bounds);
}
if (f->opdata.children_count == 0)
fprintf(out, "__top;{0}");
fprintf(out, ")");
break;
case KIND_ALT:
......@@ -396,8 +398,9 @@ void writePWF(formula_t *f, FILE *out, long long *bounds) {
for (int i = 0; i < f->opdata.children_count; i++) {
if (i > 0) fprintf(out, " U ");
writePWF(f->children + i, out, bounds);
}
if (f->opdata.children_count == 0)
fprintf(out, "__top;{0}");
fprintf(out, ")");
break;
case KIND_LOOP:
......
......@@ -135,7 +135,15 @@ int main(int argc, char **argv) {
fix_virtualized_loopinfo(entry);
FILE *pwf_file = fopen(argv[2], "w");
long long *loop_bounds = (long long*) malloc(sizeof(long long)*max_loop_id + 1);
for (CFGCollection::Iter iter(*coll); iter(); iter ++)
for (CFG::BlockIter iter2((*iter)->blocks()); iter2(); iter2++)
if (LOOP_HEADER(*iter2))
if ((*iter2)->id() > max_loop_id)
max_loop_id = (*iter2)->id();
long long *loop_bounds = (long long*) malloc(sizeof(long long)*(max_loop_id + 1));
for (int i = 0; i <= max_loop_id; i++)
loop_bounds[i] = -1;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment