Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Precise bitindex #23

Merged
merged 56 commits into from
Aug 6, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
56 commits
Select commit Hold shift + click to select a range
6c40aa7
verified appendNBits and appendNBitsLoops
samuelchassot May 17, 2024
dfcd9fe
remove lemma call
samuelchassot May 17, 2024
99e4d40
working on the verification of bitstream
samuelchassot May 21, 2024
5700419
- proved invertability of appendNLeastSignificantBits with its corres…
samuelchassot May 22, 2024
05e9617
verify invertibility appendBitsLSBFirst, with its corresponding lemma
samuelchassot May 22, 2024
35a2f90
working on proving appendBitsMSBFirstLoop, before moving to the list …
samuelchassot Jun 5, 2024
0375f5e
proved invertibility of appendBitsMSBFirst but with a List specificat…
samuelchassot Jun 7, 2024
17c39dd
verification script + stainless conf
samuelchassot Jun 7, 2024
9a95132
verified BitStream
samuelchassot Jun 10, 2024
c6d6ec9
Inverse for byte writing functions in bitstream (#5)
samuelchassot Jun 20, 2024
457645a
add scripts to verify and run genc
samuelchassot Jun 21, 2024
c6db454
Sketching precise size computation
mario-bucev Apr 29, 2024
106dacb
Rework ProofAst
mario-bucev Apr 29, 2024
4cf40e0
Simplify size fns when size is invariant
mario-bucev Apr 29, 2024
ee659d3
Add Asn1AcnAst type to SequenceChildProps, use precise size in post-c…
mario-bucev Apr 30, 2024
9864425
Wrap inlined ACN encode/decode in opaque local functions
mario-bucev May 1, 2024
34dc554
pre/postcondition for inner functions
mario-bucev May 1, 2024
dee9a09
Size computation for options
mario-bucev May 1, 2024
7dd9b4e
Add class invariants and fix size computation
mario-bucev May 2, 2024
0eddf35
Do not add alignment when computing lower bound size
mario-bucev May 6, 2024
bf77377
Bind field size computation in preparation for alignment computation
mario-bucev May 6, 2024
58c838b
Size lemmas, proofs to be done
mario-bucev May 12, 2024
6f77b32
Proofs for size lemmas
mario-bucev May 14, 2024
c3b5054
Fixing size proof gen
mario-bucev May 15, 2024
f5fc1a9
Refactor code for sequence proof gen
mario-bucev May 16, 2024
f3afa3e
Wrapping other inlined code
mario-bucev May 16, 2024
c70be08
Precise bitindex for sequences
mario-bucev May 18, 2024
db8721f
Sketching capability of generating auxiliary functions
mario-bucev May 18, 2024
67a21bc
Transform while-loops of SequenceOf to outer recursive function
mario-bucev May 22, 2024
4ca0777
Rework a bit the proof gen for sequences
mario-bucev May 30, 2024
3cf2d3c
Extract optional fields into functions
mario-bucev May 31, 2024
c9464f0
Increase stack size
mario-bucev Jun 5, 2024
1fb6d98
Remove unnecessary code and fix tests
mario-bucev Jun 6, 2024
3cf07b2
Sketching parameterizing ACN dependencies for decoding functions
mario-bucev Jun 10, 2024
e595184
Parameterization for ACN encoding functions
mario-bucev Jun 14, 2024
06bfde9
Fixing some specs
mario-bucev Jun 21, 2024
77d3318
Add IsConstraintValid to decode postcondition
mario-bucev Jun 24, 2024
c9780c0
Loop into recursive functions for strings as well
mario-bucev Jun 24, 2024
dc0156b
Change Scala ATC to construct values instead of mutating them
mario-bucev Jun 26, 2024
7dc38d7
Fix Scala UPER
mario-bucev Jun 26, 2024
8ff5dfa
Sketching conversion to List
mario-bucev Jun 28, 2024
3541a6a
Replace List with Vector
mario-bucev Jul 9, 2024
7461979
Convert strings to use Vector as well
mario-bucev Jul 9, 2024
145a51b
Generate apply methods for Sequence type alias
mario-bucev Jul 11, 2024
d0bb1cc
Add more proof annotations for SequenceOf encoding functions
mario-bucev Jul 11, 2024
13a8935
Use 0 as minimum size for size definitions
mario-bucev Jul 11, 2024
107a6b7
Add some lemmas back
mario-bucev Jul 11, 2024
faea85e
Add pre and postcondition for string types
mario-bucev Jul 12, 2024
71d4238
Make decodeUnconstrainedNumber return an option
mario-bucev Jul 12, 2024
7be92b0
Validate number length in decodeUnconstrainedWholeNumber
mario-bucev Jul 12, 2024
4d8bf33
Fix size offsetting for presence bits
mario-bucev Jul 14, 2024
9bbbbc7
Do not emit size assertions for nested sequences
mario-bucev Jul 17, 2024
32a5d59
Merge remote-tracking branch 'maxime/master' into precise-bitindex
mario-bucev Jul 17, 2024
b7924dd
Fix wrapAcnFuncBody being called when it should not
mario-bucev Jul 17, 2024
423619f
Fix string enc/dec for Scala
mario-bucev Jul 22, 2024
30990ad
Update Stainless library
mario-bucev Jul 22, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
494 changes: 251 additions & 243 deletions BackendAst/DAstACN.fs

Large diffs are not rendered by default.

30 changes: 19 additions & 11 deletions BackendAst/DAstConstruction.fs
Original file line number Diff line number Diff line change
Expand Up @@ -81,18 +81,26 @@ let private createAcnChild (r:Asn1AcnAst.AstRoot) (icdStgFileName:string) (deps:
| Asn1AcnAst.AcnReferenceToIA5String s ->
lm.lg.initializeString (int (s.str.maxSize.acn + 1I))

let rec dealiasDeps (dep: Asn1AcnAst.AcnDependency): Asn1AcnAst.AcnDependency =
match dep.dependencyKind with
| Asn1AcnAst.AcnDepRefTypeArgument param ->
let dealiased = dealiasDeps (deps.acnDependencies |> List.find (fun dep -> dep.determinant.id = param.id))
{dep with dependencyKind = dealiased.dependencyKind}
| _ -> dep

let dealiasedDeps = deps.acnDependencies |> List.filter(fun d -> d.determinant.id = ch.id) |> List.map dealiasDeps
let ret =
{

AcnChild.Name = ch.Name
id = ch.id
c_name = c_name
Type = ch.Type
AcnChild.Name = ch.Name
id = ch.id
c_name = c_name
Type = ch.Type
typeDefinitionBodyWithinSeq = tdBodyWithinSeq
funcBody = DAstACN.handleAlignmentForAcnTypes r lm acnAlignment newFuncBody
funcUpdateStatement = funcUpdateStatement
Comments = ch.Comments
initExpression = initExpression
funcBody = DAstACN.handleAlignmentForAcnTypes r lm acnAlignment newFuncBody
funcUpdateStatement = funcUpdateStatement
Comments = ch.Comments
deps = { acnDependencies = dealiasedDeps }
initExpression = initExpression
}
AcnChild ret, ns3

Expand Down Expand Up @@ -556,7 +564,7 @@ let private createTimeType (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (m:Asn1Ac

let private createSequenceOf (r:Asn1AcnAst.AstRoot) (deps:Asn1AcnAst.AcnInsertedFieldDependencies) (lm:LanguageMacros) (m:Asn1AcnAst.Asn1Module) (pi : Asn1Fold.ParentInfo<ParentInfoData> option) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.SequenceOf) (childType:Asn1Type, us:State) =
let newPrms, us0 = t.acnParameters |> foldMap(fun ns p -> mapAcnParameter r deps lm m t p ns) us
let defOrRef = DAstTypeDefinition.createSequenceOf_u r lm t o childType.typeDefinitionOrReference us0
let defOrRef = DAstTypeDefinition.createSequenceOf_u r lm t o childType us0
//let typeDefinition = DAstTypeDefinition.createSequenceOf r l t o childType.typeDefinition us0
let equalFunction = DAstEqual.createSequenceOfEqualFunction r lm t o defOrRef childType
let initFunction = DAstInitialize.createSequenceOfInitFunc r lm t o defOrRef childType
Expand Down Expand Up @@ -607,9 +615,9 @@ let private createAsn1Child (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (m:Asn1A
_ada_name = ch._ada_name
Type = newChildType
Optionality = ch.Optionality
// acnArgs = ch.acnArgs
Comments = ch.Comments |> Seq.toArray
isEqualBodyStats = DAstEqual.isEqualBodySequenceChild lm ch newChildType
//isValidBodyStats = DAstValidate.isValidSequenceChild l ch newChildType
}
Asn1Child ret, us

Expand Down
252 changes: 153 additions & 99 deletions BackendAst/DAstInitialize.fs

Large diffs are not rendered by default.

90 changes: 47 additions & 43 deletions BackendAst/DAstTypeDefinition.fs
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ let createString (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1T
let td = lm.lg.getStrTypeDefinition o.typeDef
match td.kind with
| NonPrimitiveNewTypeDefinition ->
let completeDefinition = define_new_ia5string td (o.minSize.uper) (o.maxSize.uper) ((o.maxSize.uper + 1I)) arrnAlphaChars
let completeDefinition = define_new_ia5string td o.minSize.uper o.maxSize.uper (o.maxSize.uper + 1I) arrnAlphaChars
Some completeDefinition
| NonPrimitiveNewSubTypeDefinition subDef ->
let otherProgramUnit = if td.programUnit = subDef.programUnit then None else (Some subDef.programUnit)
Expand All @@ -190,10 +190,11 @@ let createOctetString (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.
let define_new_octet_string = lm.typeDef.Define_new_octet_string
let define_subType_octet_string = lm.typeDef.Define_subType_octet_string
match td.kind with
| NonPrimitiveNewTypeDefinition ->
let completeDefinition = define_new_octet_string td (o.minSize.uper) (o.maxSize.uper) (o.minSize.uper = o.maxSize.uper)
| NonPrimitiveNewTypeDefinition ->
let invariants = lm.lg.generateOctetStringInvariants t o
let completeDefinition = define_new_octet_string td o.minSize.uper o.maxSize.uper (o.minSize.uper = o.maxSize.uper) invariants
Some completeDefinition
| NonPrimitiveNewSubTypeDefinition subDef ->
| NonPrimitiveNewSubTypeDefinition subDef ->
let otherProgramUnit = if td.programUnit = subDef.programUnit then None else (Some subDef.programUnit)
let completeDefinition = define_subType_octet_string td subDef otherProgramUnit (o.minSize.uper = o.maxSize.uper)
Some completeDefinition
Expand All @@ -220,7 +221,8 @@ let createBitString (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.As
let sComment = sprintf "(1 << %A)" nb.resolvedValue
define_named_bit td (ToC (nb.Name.Value.ToUpper())) hexValue sComment
)
let completeDefinition = define_new_bit_string td (o.minSize.uper) (o.maxSize.uper) (o.minSize.uper = o.maxSize.uper) (BigInteger o.MaxOctets) nblist
let invariants = lm.lg.generateBitStringInvariants t o
let completeDefinition = define_new_bit_string td o.minSize.uper o.maxSize.uper (o.minSize.uper = o.maxSize.uper) (BigInteger o.MaxOctets) nblist invariants
Some completeDefinition
| NonPrimitiveNewSubTypeDefinition subDef ->
let otherProgramUnit = if td.programUnit = subDef.programUnit then None else (Some subDef.programUnit)
Expand Down Expand Up @@ -248,7 +250,7 @@ let createEnumerated (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.A
match td.kind with
| NonPrimitiveNewTypeDefinition ->
let completeDefinition = define_new_enumerated td arrsEnumNames arrsEnumNamesAndValues nIndexMax macros
let privateDefinition =
let privateDefinition =
match r.args.isEnumEfficientEnabled o.items.Length with
| false -> None
| true ->
Expand All @@ -261,7 +263,7 @@ let createEnumerated (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.A
| NonPrimitiveNewSubTypeDefinition subDef ->
let otherProgramUnit = if td.programUnit = subDef.programUnit then None else (Some subDef.programUnit)
let completeDefinition = define_subType_enumerated td subDef otherProgramUnit
let privateDefinition =
let privateDefinition =
match r.args.isEnumEfficientEnabled o.items.Length with
| false -> None
| true ->
Expand All @@ -278,32 +280,34 @@ let internal getChildDefinition (childDefinition:TypeDefinitionOrReference) =
| ReferenceToExistingDefinition ref -> None


let createSequenceOf (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.SequenceOf) (childDefinition:TypeDefinitionOrReference) (us:State) =
let createSequenceOf (r: Asn1AcnAst.AstRoot) (lm: LanguageMacros) (t: Asn1AcnAst.Asn1Type) (o: Asn1AcnAst.SequenceOf) (childType: DAst.Asn1Type) (us: State) =
let define_new_sequence_of = lm.typeDef.Define_new_sequence_of
let define_subType_sequence_of = lm.typeDef.Define_subType_sequence_of
let td = lm.lg.getSizeableTypeDefinition o.typeDef

match td.kind with
| NonPrimitiveNewTypeDefinition ->
let completeDefinition = define_new_sequence_of td (o.minSize.uper) (o.maxSize.uper) (o.minSize.uper = o.maxSize.uper) (childDefinition.longTypedefName2 lm.lg.hasModules) (getChildDefinition childDefinition)
let privateDefinition =
match childDefinition with
| NonPrimitiveNewTypeDefinition ->
let invariants = lm.lg.generateSequenceOfInvariants t o childType.Kind
let sizeClsDefinitions, sizeObjDefinitions = lm.lg.generateSequenceOfSizeDefinitions t o childType
let completeDefinition = define_new_sequence_of td o.minSize.uper o.maxSize.uper (o.minSize.uper = o.maxSize.uper) (childType.typeDefinitionOrReference.longTypedefName2 lm.lg.hasModules) (getChildDefinition childType.typeDefinitionOrReference) sizeClsDefinitions sizeObjDefinitions invariants
let privateDefinition =
match childType.typeDefinitionOrReference with
| TypeDefinition td -> td.privateTypeDefinition
| ReferenceToExistingDefinition ref -> None
Some (completeDefinition, privateDefinition)
| NonPrimitiveNewSubTypeDefinition subDef ->
| NonPrimitiveNewSubTypeDefinition subDef ->
let otherProgramUnit = if td.programUnit = subDef.programUnit then None else (Some subDef.programUnit)
let completeDefinition = define_subType_sequence_of td subDef otherProgramUnit (o.minSize.uper = o.maxSize.uper) (getChildDefinition childDefinition)
let privateDefinition =
match childDefinition with
let completeDefinition = define_subType_sequence_of td subDef otherProgramUnit (o.minSize.uper = o.maxSize.uper) (getChildDefinition childType.typeDefinitionOrReference)
let privateDefinition =
match childType.typeDefinitionOrReference with
| TypeDefinition td -> td.privateTypeDefinition
| ReferenceToExistingDefinition ref -> None
Some (completeDefinition, privateDefinition)
| NonPrimitiveReference2OtherType -> None
| NonPrimitiveReference2OtherType -> None



let createSequence (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.Sequence) (allchildren:SeqChildInfo list) (us:State) =
let createSequence (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.Sequence) (allchildren: SeqChildInfo list) (us:State) =
let define_new_sequence = lm.typeDef.Define_new_sequence
let define_new_sequence_child = lm.typeDef.Define_new_sequence_child
let define_new_sequence_child_bit = lm.typeDef.Define_new_sequence_child_bit
Expand Down Expand Up @@ -336,48 +340,49 @@ let createSequence (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1
| false -> children |> List.map (fun o -> define_new_sequence_child (lm.lg.getAsn1ChildBackendName o) (o.Type.typeDefinitionOrReference.longTypedefName2 lm.lg.hasModules) o.Optionality.IsSome)

let childrenPrivatePart =
children |>
children |>
List.choose (fun o ->
match o.Type.typeDefinitionOrReference with
| TypeDefinition td -> td.privateTypeDefinition
| ReferenceToExistingDefinition ref -> None)


let arrsOptionalChildren = optionalChildren |> List.map(fun c -> define_new_sequence_child_bit (lm.lg.getAsn1ChildBackendName c))


match td.kind with
| NonPrimitiveNewTypeDefinition ->
let completeDefinition = define_new_sequence td arrsChildren arrsOptionalChildren childrenCompleteDefinitions arrsNullFieldsSavePos
let privateDef =
| NonPrimitiveNewTypeDefinition ->
let invariants = lm.lg.generateSequenceInvariants t o allchildren
let sizeDefinitions = lm.lg.generateSequenceSizeDefinitions t o allchildren
let completeDefinition = define_new_sequence td arrsChildren arrsOptionalChildren childrenCompleteDefinitions arrsNullFieldsSavePos sizeDefinitions invariants
let privateDef =
match childrenPrivatePart with
| [] -> None
| _ -> Some (childrenPrivatePart |> Seq.StrJoin "\n")
Some (completeDefinition, privateDef)
| NonPrimitiveNewSubTypeDefinition subDef ->
| NonPrimitiveNewSubTypeDefinition subDef ->
let otherProgramUnit = if td.programUnit = subDef.programUnit then None else (Some subDef.programUnit)
let completeDefinition = define_subType_sequence td subDef otherProgramUnit arrsOptionalChildren
let extraDefs = lm.lg.generateSequenceSubtypeDefinitions subDef.typeName t o children
let completeDefinition = define_subType_sequence td subDef otherProgramUnit arrsOptionalChildren extraDefs
Some (completeDefinition, None)
| NonPrimitiveReference2OtherType -> None
| NonPrimitiveReference2OtherType -> None




let createChoice (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.Choice) (children:ChChildInfo list) (us:State) =
let createChoice (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.Choice) (children:ChChildInfo list) (us:State) =
let define_new_choice = lm.typeDef.Define_new_choice
let define_new_choice_child = lm.typeDef.Define_new_choice_child
let define_subType_choice = lm.typeDef.Define_subType_choice


let td = lm.lg.getChoiceTypeDefinition o.typeDef
let childldrenCompleteDefinitions = children |> List.choose (fun c -> getChildDefinition c.chType.typeDefinitionOrReference)
let childrenCompleteDefinitions = children |> List.choose (fun c -> getChildDefinition c.chType.typeDefinitionOrReference)
let arrsPresent = children |> List.map(fun c -> lm.lg.presentWhenName None c)
let arrsChildren = children |> List.map (fun o -> define_new_choice_child (lm.lg.getAsn1ChChildBackendName o) (o.chType.typeDefinitionOrReference.longTypedefName2 lm.lg.hasModules) (lm.lg.presentWhenName None o))
let arrsChildren = children |> List.map (fun o -> define_new_choice_child (lm.lg.getAsn1ChChildBackendName o) (o.chType.typeDefinitionOrReference.longTypedefName2 lm.lg.hasModules) (lm.lg.presentWhenName None o))
let arrsCombined = List.map2 (fun x y -> x + "(" + y + ")") arrsPresent arrsChildren
let nIndexMax = BigInteger ((Seq.length children)-1)

let privatePart =
let childPrivateParts = children |>
let childPrivateParts = children |>
List.choose(fun o ->
match o.chType.typeDefinitionOrReference with
| TypeDefinition td -> td.privateTypeDefinition
Expand All @@ -388,14 +393,15 @@ let createChoice (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Ty


match td.kind with
| NonPrimitiveNewTypeDefinition ->
let completeDefinition = define_new_choice td (lm.lg.choiceIDForNone us.typeIdsSet t.id) (lm.lg.presentWhenName None children.Head) arrsChildren arrsPresent arrsCombined nIndexMax childldrenCompleteDefinitions
| NonPrimitiveNewTypeDefinition ->
let sizeDefinitions = lm.lg.generateChoiceSizeDefinitions t o children
let completeDefinition = define_new_choice td (lm.lg.choiceIDForNone us.typeIdsSet t.id) (lm.lg.presentWhenName None children.Head) arrsChildren arrsPresent arrsCombined nIndexMax childrenCompleteDefinitions sizeDefinitions
Some (completeDefinition, privatePart)
| NonPrimitiveNewSubTypeDefinition subDef ->
| NonPrimitiveNewSubTypeDefinition subDef ->
let otherProgramUnit = if td.programUnit = subDef.programUnit then None else (Some subDef.programUnit)
let completeDefinition = define_subType_choice td subDef otherProgramUnit
Some (completeDefinition, None)
| NonPrimitiveReference2OtherType -> None
| NonPrimitiveReference2OtherType -> None


////////////////////////////////
Expand Down Expand Up @@ -536,7 +542,7 @@ let createString_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn


let createEnumerated_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.Enumerated) (us:State) =
let (aaa, priv) =
let (aaa, priv) =
match createEnumerated r lm t o us with
| Some (a, b) -> Some a, b
| None -> None, None
Expand All @@ -552,9 +558,9 @@ let createEnumerated_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst
ReferenceToExistingDefinition {ReferenceToExistingDefinition.programUnit = (if td.programUnit = programUnit then None else Some td.programUnit); typedefName= td.typeName; definedInRtl = false}


let createSequenceOf_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.SequenceOf) (childDefinition:TypeDefinitionOrReference) (us:State) =
let aaa, privateDef =
match createSequenceOf r lm t o childDefinition us with
let createSequenceOf_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.SequenceOf) (childType: DAst.Asn1Type) (us:State) =
let aaa, privateDef =
match createSequenceOf r lm t o childType us with
| Some (a, b) -> Some a, b
| None -> None, None
let programUnit = ToC t.id.ModName
Expand All @@ -570,7 +576,7 @@ let createSequenceOf_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst


let createSequence_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.Sequence) (children:SeqChildInfo list) (us:State) =
let aaa, private_part =
let aaa, private_part =
match createSequence r lm t o children us with
| Some (a, b) -> Some a, b
| None -> None, None
Expand All @@ -586,7 +592,7 @@ let createSequence_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.A
ReferenceToExistingDefinition {ReferenceToExistingDefinition.programUnit = (if td.programUnit = programUnit then None else Some td.programUnit); typedefName= td.typeName; definedInRtl = false}

let createChoice_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnAst.Asn1Type) (o:Asn1AcnAst.Choice) (children:ChChildInfo list) (us:State) =
let aaa, private_part =
let aaa, private_part =
match createChoice r lm t o children us with
| Some (a, b) -> Some a, b
| None -> None, None
Expand All @@ -606,5 +612,3 @@ let createReferenceType_u (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1AcnA
match o.encodingOptions with
| None -> baseType.typeDefinitionOrReference
| Some _ -> baseType.typeDefinitionOrReference


Loading
Loading