aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintLTL.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-04-02 16:25:25 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-04-02 16:25:25 +0200
commit170284b51766112e29d6bbfe519bad9f6da95269 (patch)
tree13a163ccee48cee0512a8af484b394623cdce030 /backend/PrintLTL.ml
parent2e30ad9698a6f24a8a746f68b30c235913006392 (diff)
parent959432fa13a899290db5236f93575a8bfdc13bb5 (diff)
downloadcompcert-170284b51766112e29d6bbfe519bad9f6da95269.tar.gz
compcert-170284b51766112e29d6bbfe519bad9f6da95269.zip
Merge branch 'master' into dwarf
Diffstat (limited to 'backend/PrintLTL.ml')
-rw-r--r--backend/PrintLTL.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index 52e51309..27936f9b 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -81,8 +81,8 @@ let print_instruction pp succ = function
fprintf pp "%a = %s(%a)"
mregs res (name_of_external ef) mregs args
| Lannot(ef, args) ->
- fprintf pp "%s(%a)"
- (name_of_external ef) locs args
+ fprintf pp "%s(%a)\n"
+ (name_of_external ef) (print_annot_args loc) args
| Lbranch s ->
print_succ pp s succ
| Lcond(cond, args, s1, s2) ->