fix dummy symbol creation

Author: redianthus

shell.nix

@@ -8,8 +8,8 @@ let
     src = pkgs.fetchFromGitHub {
       owner = "redianthus";
       repo = "smtml";
-      rev = "b8853d3a589722652904dfc1d6f85958f954dd4c";
-      hash = "sha256-9ogUDfsUbHsEfMhxdfA/bvUVLy4oxBT7pXnGQkPiLkY=";
+      rev = "25a307e685b79ef772266a76070922dfdb25bd80";
+      hash = "sha256-BgsX69fTCPc3ScTmiDpeScem+k6CJ+61RIdoSVp2At4=";
     };
   });
   synchronizer = pkgs.ocamlPackages.synchronizer.overrideAttrs (old: {

src/symbolic/symbol_scope.ml

@@ -40,20 +40,16 @@ let get_value model sym ty =
   | Some v -> v
   | None -> (
     (* The symbol was created but is not part of the generated model. Thus we can use a dummy value. TODO: allows to hide these symbols or their value through a flag (and make it the default, the flag should actually display them). *)
+    (* TODO: do this in Smt.ml, see https://github.com/formalsec/smtml/issues/483 *)
     let res =
       match ty with
       | Smtml.Ty.Ty_bool -> Smtml.Value.of_string ty "false"
-      | Ty_bitv 8 ->
-        Ok (Smtml.Value.Bitv (Smtml.Bitvector.make (Z.of_string "0") 8))
-      | Ty_bitv 32 ->
-        Ok (Smtml.Value.Bitv (Smtml.Bitvector.make (Z.of_string "0") 32))
-      | Ty_bitv 64 ->
-        Ok (Smtml.Value.Bitv (Smtml.Bitvector.make (Z.of_string "0") 64))
+      | Ty_bitv n ->
+        Ok (Smtml.Value.Bitv (Smtml.Bitvector.make (Z.of_string "0") n))
       | Ty_fp 32 -> Smtml.Value.of_string ty "0.0"
       | Ty_fp 64 -> Smtml.Value.of_string ty "0.0"
-      | ty ->
-        Log.err (fun m ->
-          m "unhandled type %a in symbol_scope.ml" Smtml.Ty.pp ty );
+      | _ty ->
+        (* if this fails, it may be that we changed something and a new type should be added here *)
         assert false
     in
     match res with Ok v -> v | Error _ -> assert false )