summaryrefslogtreecommitdiff
path: root/src/CfimOfJson.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-29 20:30:16 +0100
committerSon Ho2022-01-29 20:30:16 +0100
commit79af7f999e3a41e3c5f9a30819a7cc43b5397c56 (patch)
treea3b047e0b72f8f493a2395bbf47fb434d9b73205 /src/CfimOfJson.ml
parentfe5d34965d44120e491fb2fa42262d8439ea38c7 (diff)
Make the field names optional and make progress on ExtractToFStar
Diffstat (limited to 'src/CfimOfJson.ml')
-rw-r--r--src/CfimOfJson.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 82f9d95a..3378f548 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -134,7 +134,7 @@ let field_of_json (js : json) : (T.field, string) result =
combine_error_msgs js "field_of_json"
(match js with
| `Assoc [ ("name", name); ("ty", ty) ] ->
- let* name = string_of_json name in
+ let* name = option_of_json string_of_json name in
let* ty = sty_of_json ty in
Ok { T.field_name = name; field_ty = ty }
| _ -> Error "")