aboutsummaryrefslogtreecommitdiffstats
path: root/scripts
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-13 05:24:08 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-13 05:24:08 +0100
commit04b05b8039f7b306d8dacbf7bd0ec58ba7dc209d (patch)
tree51eea9a286a53caba0f9ae7dacc5285d479ea519 /scripts
parent0e423e645dba8a0f0a48e98a66aee9d53fb3a194 (diff)
downloadcompcert-kvx-04b05b8039f7b306d8dacbf7bd0ec58ba7dc209d.tar.gz
compcert-kvx-04b05b8039f7b306d8dacbf7bd0ec58ba7dc209d.zip
for using CPlex
Diffstat (limited to 'scripts')
-rwxr-xr-xscripts/cplex/ilp_solver11
1 files changed, 7 insertions, 4 deletions
diff --git a/scripts/cplex/ilp_solver b/scripts/cplex/ilp_solver
index a449c203..1e70a652 100755
--- a/scripts/cplex/ilp_solver
+++ b/scripts/cplex/ilp_solver
@@ -1,7 +1,10 @@
#!/bin/sh
tmp=$2.tmp
rm -f $tmp $2
-cplex -c "read $1" "optimize" "write $tmp sol"
-grep '<variable name="' $tmp | sed -e 's@ *<variable name="@@' -e 's@" index=.* value="@ @' -e 's@"/>@@' > $2
-touch $2
-rm -f $tmp
+if cplex -c "read $1" "optimize" "write $tmp sol";
+then
+ grep '<variable name="' $tmp | sed -e 's@ *<variable name="@@' -e 's@" index=.* value="@ @' -e 's@"/>@@' > $2
+ rm -f $tmp
+else
+ exit $?
+fi