Change handling of incomplete pattern match statements

Raise an error in case of a pattern match failure rather than allowing undefined behaviour. This better reflects the intended ASL semantics. Also remove a number of unnecessary fall-through cases that were introduced due to bugs in asl_to_sail, as reported in issue #16.
rems-project · Dec 14, 2023 · 24c0d10 · 24c0d10
1 parent bb55d77
commit 24c0d10
Show file tree

Hide file tree

Showing 9 changed files with 2,433 additions and 4,338 deletions.
diff --git a/arm-v9.4-a/coq/arm_extras.v b/arm-v9.4-a/coq/arm_extras.v
@@ -1,7 +1,7 @@
 (******************************************************************************)
 (*  BSD 3-clause Clear License                                                *)
 (*                                                                            *)
-(*  Copyright (c) 2022                                                        *)
+(*  Copyright (c) 2023                                                        *)
 (*    Arm Limited (or its affiliates),                                        *)
 (*    Thomas Bauereiss,                                                       *)
 (*    Brian Campbell,                                                         *)