aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-23 10:34:25 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-23 10:34:25 +0100
commit7d541f25751838e1cde2a292a71afaa28879b753 (patch)
tree41138314af0177e64c0b443191b69cada1e28be0 /checker
parente5b128c7d4c2fd28a4ad7c5df8e48d485cd703f3 (diff)
Bypass int and string representation in votour when it's incorrect.
Diffstat (limited to 'checker')
-rw-r--r--checker/votour.ml11
1 files changed, 10 insertions, 1 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index 38f1ff9bc..95b9f2332 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -230,7 +230,16 @@ let rec get_children v o pos = match v with
| BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|]
| _ -> raise Exit
end
- |String | Int -> [||]
+ | String ->
+ begin match Repr.repr o with
+ | STRING _ -> [||]
+ | _ -> raise Exit
+ end
+ | Int ->
+ begin match Repr.repr o with
+ | INT _ -> [||]
+ | _ -> raise Exit
+ end
|Annot (s,v) -> get_children v o pos
|Any -> raise Exit
|Dyn ->