Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8

1 files changed, 17 insertions, 6 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index 342bd8ca..8667922f 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -251,10 +251,16 @@ Function sel_known_builtin (bf: builtin_function) (args: exprlist) :=
       Some (sel_select ty a1 a2 a3)
   | BI_standard BI_fabs, a1 ::: Enil =>
       Some (SelectOp.absf a1)
+  | BI_standard BI_fabsf, a1 ::: Enil =>
+      Some (SelectOp.absfs a1)
   | _, _ =>
       None
   end.
 
+(** A CminorSel statement that does nothing, like [Sskip], but reduces. *)
+
+Definition Sno_op := Sseq Sskip Sskip.
+
 (** Builtin functions in general *)
 
 Definition sel_builtin_default (optid: option ident) (ef: external_function)
@@ -264,17 +270,22 @@ Definition sel_builtin_default (optid: option ident) (ef: external_function)
 
 Definition sel_builtin (optid: option ident) (ef: external_function)
                                (args: list Cminor.expr) :=
-  match optid, ef with
-  | Some id, EF_builtin name sg =>
+  match ef with
+  | EF_builtin name sg =>
       match lookup_builtin_function name sg with
       | Some bf =>
-          match sel_known_builtin bf (sel_exprlist args) with
-          | Some a => Sassign id a
-          | None => sel_builtin_default optid ef args
+          match optid with
+          | Some id =>
+              match sel_known_builtin bf (sel_exprlist args) with
+              | Some a => Sassign id a
+              | None => sel_builtin_default optid ef args
+              end
+          | None =>
+              Sno_op   (**r builtins with semantics are pure *)
           end
       | None => sel_builtin_default optid ef args
       end
-  | _, _ =>
+  | _ =>
       sel_builtin_default optid ef args
   end.