Initial upstream commit
The history contained unlicensed code so everything got squashed, sorry. Change-Id: Ie1335ecfcee7f740bb6de2e9887606be30a2deff Signed-off-by: Nico Huber <nico.huber@secunet.com>
This commit is contained in:
commit
5e9b1b50e7
|
@ -0,0 +1,5 @@
|
|||
/proof-allconfigs/
|
||||
/build/
|
||||
/dest/
|
||||
/*.gpr
|
||||
/.config
|
|
@ -0,0 +1,339 @@
|
|||
GNU GENERAL PUBLIC LICENSE
|
||||
Version 2, June 1991
|
||||
|
||||
Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
|
||||
51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
|
||||
Everyone is permitted to copy and distribute verbatim copies
|
||||
of this license document, but changing it is not allowed.
|
||||
|
||||
Preamble
|
||||
|
||||
The licenses for most software are designed to take away your
|
||||
freedom to share and change it. By contrast, the GNU General Public
|
||||
License is intended to guarantee your freedom to share and change free
|
||||
software--to make sure the software is free for all its users. This
|
||||
General Public License applies to most of the Free Software
|
||||
Foundation's software and to any other program whose authors commit to
|
||||
using it. (Some other Free Software Foundation software is covered by
|
||||
the GNU Lesser General Public License instead.) You can apply it to
|
||||
your programs, too.
|
||||
|
||||
When we speak of free software, we are referring to freedom, not
|
||||
price. Our General Public Licenses are designed to make sure that you
|
||||
have the freedom to distribute copies of free software (and charge for
|
||||
this service if you wish), that you receive source code or can get it
|
||||
if you want it, that you can change the software or use pieces of it
|
||||
in new free programs; and that you know you can do these things.
|
||||
|
||||
To protect your rights, we need to make restrictions that forbid
|
||||
anyone to deny you these rights or to ask you to surrender the rights.
|
||||
These restrictions translate to certain responsibilities for you if you
|
||||
distribute copies of the software, or if you modify it.
|
||||
|
||||
For example, if you distribute copies of such a program, whether
|
||||
gratis or for a fee, you must give the recipients all the rights that
|
||||
you have. You must make sure that they, too, receive or can get the
|
||||
source code. And you must show them these terms so they know their
|
||||
rights.
|
||||
|
||||
We protect your rights with two steps: (1) copyright the software, and
|
||||
(2) offer you this license which gives you legal permission to copy,
|
||||
distribute and/or modify the software.
|
||||
|
||||
Also, for each author's protection and ours, we want to make certain
|
||||
that everyone understands that there is no warranty for this free
|
||||
software. If the software is modified by someone else and passed on, we
|
||||
want its recipients to know that what they have is not the original, so
|
||||
that any problems introduced by others will not reflect on the original
|
||||
authors' reputations.
|
||||
|
||||
Finally, any free program is threatened constantly by software
|
||||
patents. We wish to avoid the danger that redistributors of a free
|
||||
program will individually obtain patent licenses, in effect making the
|
||||
program proprietary. To prevent this, we have made it clear that any
|
||||
patent must be licensed for everyone's free use or not licensed at all.
|
||||
|
||||
The precise terms and conditions for copying, distribution and
|
||||
modification follow.
|
||||
|
||||
GNU GENERAL PUBLIC LICENSE
|
||||
TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
|
||||
|
||||
0. This License applies to any program or other work which contains
|
||||
a notice placed by the copyright holder saying it may be distributed
|
||||
under the terms of this General Public License. The "Program", below,
|
||||
refers to any such program or work, and a "work based on the Program"
|
||||
means either the Program or any derivative work under copyright law:
|
||||
that is to say, a work containing the Program or a portion of it,
|
||||
either verbatim or with modifications and/or translated into another
|
||||
language. (Hereinafter, translation is included without limitation in
|
||||
the term "modification".) Each licensee is addressed as "you".
|
||||
|
||||
Activities other than copying, distribution and modification are not
|
||||
covered by this License; they are outside its scope. The act of
|
||||
running the Program is not restricted, and the output from the Program
|
||||
is covered only if its contents constitute a work based on the
|
||||
Program (independent of having been made by running the Program).
|
||||
Whether that is true depends on what the Program does.
|
||||
|
||||
1. You may copy and distribute verbatim copies of the Program's
|
||||
source code as you receive it, in any medium, provided that you
|
||||
conspicuously and appropriately publish on each copy an appropriate
|
||||
copyright notice and disclaimer of warranty; keep intact all the
|
||||
notices that refer to this License and to the absence of any warranty;
|
||||
and give any other recipients of the Program a copy of this License
|
||||
along with the Program.
|
||||
|
||||
You may charge a fee for the physical act of transferring a copy, and
|
||||
you may at your option offer warranty protection in exchange for a fee.
|
||||
|
||||
2. You may modify your copy or copies of the Program or any portion
|
||||
of it, thus forming a work based on the Program, and copy and
|
||||
distribute such modifications or work under the terms of Section 1
|
||||
above, provided that you also meet all of these conditions:
|
||||
|
||||
a) You must cause the modified files to carry prominent notices
|
||||
stating that you changed the files and the date of any change.
|
||||
|
||||
b) You must cause any work that you distribute or publish, that in
|
||||
whole or in part contains or is derived from the Program or any
|
||||
part thereof, to be licensed as a whole at no charge to all third
|
||||
parties under the terms of this License.
|
||||
|
||||
c) If the modified program normally reads commands interactively
|
||||
when run, you must cause it, when started running for such
|
||||
interactive use in the most ordinary way, to print or display an
|
||||
announcement including an appropriate copyright notice and a
|
||||
notice that there is no warranty (or else, saying that you provide
|
||||
a warranty) and that users may redistribute the program under
|
||||
these conditions, and telling the user how to view a copy of this
|
||||
License. (Exception: if the Program itself is interactive but
|
||||
does not normally print such an announcement, your work based on
|
||||
the Program is not required to print an announcement.)
|
||||
|
||||
These requirements apply to the modified work as a whole. If
|
||||
identifiable sections of that work are not derived from the Program,
|
||||
and can be reasonably considered independent and separate works in
|
||||
themselves, then this License, and its terms, do not apply to those
|
||||
sections when you distribute them as separate works. But when you
|
||||
distribute the same sections as part of a whole which is a work based
|
||||
on the Program, the distribution of the whole must be on the terms of
|
||||
this License, whose permissions for other licensees extend to the
|
||||
entire whole, and thus to each and every part regardless of who wrote it.
|
||||
|
||||
Thus, it is not the intent of this section to claim rights or contest
|
||||
your rights to work written entirely by you; rather, the intent is to
|
||||
exercise the right to control the distribution of derivative or
|
||||
collective works based on the Program.
|
||||
|
||||
In addition, mere aggregation of another work not based on the Program
|
||||
with the Program (or with a work based on the Program) on a volume of
|
||||
a storage or distribution medium does not bring the other work under
|
||||
the scope of this License.
|
||||
|
||||
3. You may copy and distribute the Program (or a work based on it,
|
||||
under Section 2) in object code or executable form under the terms of
|
||||
Sections 1 and 2 above provided that you also do one of the following:
|
||||
|
||||
a) Accompany it with the complete corresponding machine-readable
|
||||
source code, which must be distributed under the terms of Sections
|
||||
1 and 2 above on a medium customarily used for software interchange; or,
|
||||
|
||||
b) Accompany it with a written offer, valid for at least three
|
||||
years, to give any third party, for a charge no more than your
|
||||
cost of physically performing source distribution, a complete
|
||||
machine-readable copy of the corresponding source code, to be
|
||||
distributed under the terms of Sections 1 and 2 above on a medium
|
||||
customarily used for software interchange; or,
|
||||
|
||||
c) Accompany it with the information you received as to the offer
|
||||
to distribute corresponding source code. (This alternative is
|
||||
allowed only for noncommercial distribution and only if you
|
||||
received the program in object code or executable form with such
|
||||
an offer, in accord with Subsection b above.)
|
||||
|
||||
The source code for a work means the preferred form of the work for
|
||||
making modifications to it. For an executable work, complete source
|
||||
code means all the source code for all modules it contains, plus any
|
||||
associated interface definition files, plus the scripts used to
|
||||
control compilation and installation of the executable. However, as a
|
||||
special exception, the source code distributed need not include
|
||||
anything that is normally distributed (in either source or binary
|
||||
form) with the major components (compiler, kernel, and so on) of the
|
||||
operating system on which the executable runs, unless that component
|
||||
itself accompanies the executable.
|
||||
|
||||
If distribution of executable or object code is made by offering
|
||||
access to copy from a designated place, then offering equivalent
|
||||
access to copy the source code from the same place counts as
|
||||
distribution of the source code, even though third parties are not
|
||||
compelled to copy the source along with the object code.
|
||||
|
||||
4. You may not copy, modify, sublicense, or distribute the Program
|
||||
except as expressly provided under this License. Any attempt
|
||||
otherwise to copy, modify, sublicense or distribute the Program is
|
||||
void, and will automatically terminate your rights under this License.
|
||||
However, parties who have received copies, or rights, from you under
|
||||
this License will not have their licenses terminated so long as such
|
||||
parties remain in full compliance.
|
||||
|
||||
5. You are not required to accept this License, since you have not
|
||||
signed it. However, nothing else grants you permission to modify or
|
||||
distribute the Program or its derivative works. These actions are
|
||||
prohibited by law if you do not accept this License. Therefore, by
|
||||
modifying or distributing the Program (or any work based on the
|
||||
Program), you indicate your acceptance of this License to do so, and
|
||||
all its terms and conditions for copying, distributing or modifying
|
||||
the Program or works based on it.
|
||||
|
||||
6. Each time you redistribute the Program (or any work based on the
|
||||
Program), the recipient automatically receives a license from the
|
||||
original licensor to copy, distribute or modify the Program subject to
|
||||
these terms and conditions. You may not impose any further
|
||||
restrictions on the recipients' exercise of the rights granted herein.
|
||||
You are not responsible for enforcing compliance by third parties to
|
||||
this License.
|
||||
|
||||
7. If, as a consequence of a court judgment or allegation of patent
|
||||
infringement or for any other reason (not limited to patent issues),
|
||||
conditions are imposed on you (whether by court order, agreement or
|
||||
otherwise) that contradict the conditions of this License, they do not
|
||||
excuse you from the conditions of this License. If you cannot
|
||||
distribute so as to satisfy simultaneously your obligations under this
|
||||
License and any other pertinent obligations, then as a consequence you
|
||||
may not distribute the Program at all. For example, if a patent
|
||||
license would not permit royalty-free redistribution of the Program by
|
||||
all those who receive copies directly or indirectly through you, then
|
||||
the only way you could satisfy both it and this License would be to
|
||||
refrain entirely from distribution of the Program.
|
||||
|
||||
If any portion of this section is held invalid or unenforceable under
|
||||
any particular circumstance, the balance of the section is intended to
|
||||
apply and the section as a whole is intended to apply in other
|
||||
circumstances.
|
||||
|
||||
It is not the purpose of this section to induce you to infringe any
|
||||
patents or other property right claims or to contest validity of any
|
||||
such claims; this section has the sole purpose of protecting the
|
||||
integrity of the free software distribution system, which is
|
||||
implemented by public license practices. Many people have made
|
||||
generous contributions to the wide range of software distributed
|
||||
through that system in reliance on consistent application of that
|
||||
system; it is up to the author/donor to decide if he or she is willing
|
||||
to distribute software through any other system and a licensee cannot
|
||||
impose that choice.
|
||||
|
||||
This section is intended to make thoroughly clear what is believed to
|
||||
be a consequence of the rest of this License.
|
||||
|
||||
8. If the distribution and/or use of the Program is restricted in
|
||||
certain countries either by patents or by copyrighted interfaces, the
|
||||
original copyright holder who places the Program under this License
|
||||
may add an explicit geographical distribution limitation excluding
|
||||
those countries, so that distribution is permitted only in or among
|
||||
countries not thus excluded. In such case, this License incorporates
|
||||
the limitation as if written in the body of this License.
|
||||
|
||||
9. The Free Software Foundation may publish revised and/or new versions
|
||||
of the General Public License from time to time. Such new versions will
|
||||
be similar in spirit to the present version, but may differ in detail to
|
||||
address new problems or concerns.
|
||||
|
||||
Each version is given a distinguishing version number. If the Program
|
||||
specifies a version number of this License which applies to it and "any
|
||||
later version", you have the option of following the terms and conditions
|
||||
either of that version or of any later version published by the Free
|
||||
Software Foundation. If the Program does not specify a version number of
|
||||
this License, you may choose any version ever published by the Free Software
|
||||
Foundation.
|
||||
|
||||
10. If you wish to incorporate parts of the Program into other free
|
||||
programs whose distribution conditions are different, write to the author
|
||||
to ask for permission. For software which is copyrighted by the Free
|
||||
Software Foundation, write to the Free Software Foundation; we sometimes
|
||||
make exceptions for this. Our decision will be guided by the two goals
|
||||
of preserving the free status of all derivatives of our free software and
|
||||
of promoting the sharing and reuse of software generally.
|
||||
|
||||
NO WARRANTY
|
||||
|
||||
11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
|
||||
FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN
|
||||
OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
|
||||
PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
|
||||
OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
|
||||
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS
|
||||
TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE
|
||||
PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
|
||||
REPAIR OR CORRECTION.
|
||||
|
||||
12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
|
||||
WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
|
||||
REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
|
||||
OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
|
||||
TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
|
||||
YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
|
||||
PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
|
||||
POSSIBILITY OF SUCH DAMAGES.
|
||||
|
||||
END OF TERMS AND CONDITIONS
|
||||
|
||||
How to Apply These Terms to Your New Programs
|
||||
|
||||
If you develop a new program, and you want it to be of the greatest
|
||||
possible use to the public, the best way to achieve this is to make it
|
||||
free software which everyone can redistribute and change under these terms.
|
||||
|
||||
To do so, attach the following notices to the program. It is safest
|
||||
to attach them to the start of each source file to most effectively
|
||||
convey the exclusion of warranty; and each file should have at least
|
||||
the "copyright" line and a pointer to where the full notice is found.
|
||||
|
||||
<one line to give the program's name and a brief idea of what it does.>
|
||||
Copyright (C) <year> <name of author>
|
||||
|
||||
This program is free software; you can redistribute it and/or modify
|
||||
it under the terms of the GNU General Public License as published by
|
||||
the Free Software Foundation; either version 2 of the License, or
|
||||
(at your option) any later version.
|
||||
|
||||
This program is distributed in the hope that it will be useful,
|
||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
GNU General Public License for more details.
|
||||
|
||||
You should have received a copy of the GNU General Public License along
|
||||
with this program; if not, write to the Free Software Foundation, Inc.,
|
||||
51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
|
||||
|
||||
Also add information on how to contact you by electronic and paper mail.
|
||||
|
||||
If the program is interactive, make it output a short notice like this
|
||||
when it starts in an interactive mode:
|
||||
|
||||
Gnomovision version 69, Copyright (C) year name of author
|
||||
Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
|
||||
This is free software, and you are welcome to redistribute it
|
||||
under certain conditions; type `show c' for details.
|
||||
|
||||
The hypothetical commands `show w' and `show c' should show the appropriate
|
||||
parts of the General Public License. Of course, the commands you use may
|
||||
be called something other than `show w' and `show c'; they could even be
|
||||
mouse-clicks or menu items--whatever suits your program.
|
||||
|
||||
You should also get your employer (if you work as a programmer) or your
|
||||
school, if any, to sign a "copyright disclaimer" for the program, if
|
||||
necessary. Here is a sample; alter the names:
|
||||
|
||||
Yoyodyne, Inc., hereby disclaims all copyright interest in the program
|
||||
`Gnomovision' (which makes passes at compilers) written by James Hacker.
|
||||
|
||||
<signature of Ty Coon>, 1 April 1989
|
||||
Ty Coon, President of Vice
|
||||
|
||||
This General Public License does not permit incorporating your program into
|
||||
proprietary programs. If your program is a subroutine library, you may
|
||||
consider it more useful to permit linking proprietary applications with the
|
||||
library. If this is what you want to do, use the GNU Lesser General
|
||||
Public License instead of this License.
|
|
@ -0,0 +1,268 @@
|
|||
libhw-dir := $(dir $(lastword $(MAKEFILE_LIST)))
|
||||
|
||||
DESTDIR ?= dest
|
||||
|
||||
name ?= hw
|
||||
hw-install = Makefile Makefile.proof gnat.adc spark.adc
|
||||
|
||||
top := $(CURDIR)
|
||||
cnf := .config
|
||||
obj := build
|
||||
|
||||
binary := $(obj)/lib$(name).a
|
||||
$(binary):
|
||||
|
||||
space :=
|
||||
space +=
|
||||
comma := ,
|
||||
|
||||
$(foreach dep,$($(name)-deplibs), \
|
||||
$(eval -include $($(dep)-dir)/config))
|
||||
-include $(cnf)
|
||||
|
||||
include $(libhw-dir)/Makefile.proof
|
||||
|
||||
CC = $(CROSS_COMPILE)gcc
|
||||
GNATBIND = $(CROSS_COMPILE)gnatbind
|
||||
|
||||
ADAFLAGS += -gnatA -gnatec=$(libhw-dir)/gnat.adc
|
||||
ADAFLAGS += -gnatg -gnatp
|
||||
ADAFLAGS += -Wuninitialized -Wall -Werror
|
||||
ADAFLAGS += -pipe -g
|
||||
ADAFLAGS += -Wstrict-aliasing -Wshadow
|
||||
ADAFLAGS += -fno-common -fomit-frame-pointer
|
||||
ADAFLAGS += -ffunction-sections -fdata-sections
|
||||
# Ada warning options:
|
||||
#
|
||||
# a Activate most optional warnings.
|
||||
# .e Activate every optional warnings.
|
||||
# e Treat warnings and style checks as errors.
|
||||
#
|
||||
# D Suppress warnings on implicit dereferences:
|
||||
# As SPARK does not accept access types we have to map the
|
||||
# dynamically chosen register locations to a static SPARK
|
||||
# variable.
|
||||
#
|
||||
# .H Suppress warnings on holes/gaps in records:
|
||||
# We are modelling hardware here!
|
||||
#
|
||||
# H Suppress warnings on hiding:
|
||||
# It's too annoying, you run out of ideas for identifiers fast.
|
||||
#
|
||||
# T Suppress warnings for tracking of deleted conditional code:
|
||||
# We use static options to select code paths at compile time.
|
||||
#
|
||||
# U Suppress warnings on unused entities:
|
||||
# Would have lots of warnings for unused register definitions,
|
||||
# `withs` for debugging etc.
|
||||
#
|
||||
# .U Deactivate warnings on unordered enumeration types:
|
||||
# As SPARK doesn't support `pragma Ordered` by now, we don't
|
||||
# use that, yet.
|
||||
#
|
||||
# .W Suppress warnings on unnecessary Warnings Off pragmas:
|
||||
# Things get really messy when you use different compiler
|
||||
# versions, otherwise.
|
||||
# .Y Disable information messages for why package spec needs body:
|
||||
# Those messages are annoying. But don't forget to enable those,
|
||||
# if you need the information.
|
||||
ADAFLAGS += -gnatwa.eeD.HHTU.U.W.Y
|
||||
# Disable style checks for now
|
||||
ADAFLAGS += -gnatyN
|
||||
|
||||
MAKEFLAGS += -rR
|
||||
|
||||
# Make is silent per default, but 'make V=1' will show all compiler calls.
|
||||
ifneq ($(V),1)
|
||||
.SILENT:
|
||||
endif
|
||||
|
||||
# must come rather early
|
||||
.SECONDEXPANSION:
|
||||
|
||||
$(binary): $$($(name)-objs)
|
||||
@printf " AR $(subst $(obj)/,,$@)\n"
|
||||
ar cr $@ $^
|
||||
|
||||
$(foreach dep,$($(name)-deplibs), \
|
||||
$(eval $(name)-extra-objs += $($(dep)-dir)/lib) \
|
||||
$(eval $(name)-extra-incs += $($(dep)-dir)/include))
|
||||
|
||||
# Converts one or more source file paths to their corresponding build/ paths.
|
||||
# Only .ads and .adb get converted to .o, other files keep their names.
|
||||
# $1 file path (list)
|
||||
src-to-obj = \
|
||||
$(addprefix $(obj)/,\
|
||||
$(patsubst $(obj)/%,%, \
|
||||
$(patsubst %.ads,%.o,\
|
||||
$(patsubst %.adb,%.o,\
|
||||
$(2)))))
|
||||
|
||||
# Converts one or more source file paths to the corresponding build/ paths
|
||||
# of their Ada library information (.ali) files.
|
||||
# $1 file path (list)
|
||||
src-to-ali = \
|
||||
$(addprefix $(obj)/,\
|
||||
$(patsubst $(obj)/%,%, \
|
||||
$(patsubst %.ads,%.ali,\
|
||||
$(patsubst %.adb,%.ali,\
|
||||
$(filter %.ads %.adb,$(2))))))
|
||||
|
||||
# Clean -y variables, include Makefile.inc
|
||||
# Add paths to files in $(name)-y to $(name)-srcs
|
||||
# Add subdirs-y to subdirs
|
||||
# $1 dir to read Makefile.inc from
|
||||
includemakefile = \
|
||||
$(eval $(name)-y :=) \
|
||||
$(eval $(name)-gen-y :=) \
|
||||
$(eval $(name)-proof-y :=) \
|
||||
$(eval subdirs-y :=) \
|
||||
$(eval include $(1)/Makefile.inc) \
|
||||
$(eval $(name)-srcs += \
|
||||
$(subst $(top)/,, \
|
||||
$(abspath $(addprefix $(1)/,$($(name)-y))))) \
|
||||
$(eval $(name)-gens += \
|
||||
$(subst $(top)/,, \
|
||||
$(abspath $($(name)-gen-y)))) \
|
||||
$(eval $(name)-proof += \
|
||||
$(subst $(top)/,, \
|
||||
$(abspath $(addprefix $(1)/,$($(name)-proof-y))))) \
|
||||
$(eval subdirs += \
|
||||
$(subst $(top)/,, \
|
||||
$(abspath $(addprefix $(1)/,$(subdirs-y))))) \
|
||||
|
||||
# For each path in $(subdirs) call includemakefiles
|
||||
# Repeat until subdirs is empty
|
||||
evaluate_subdirs = \
|
||||
$(eval cursubdirs := $(subdirs)) \
|
||||
$(eval subdirs :=) \
|
||||
$(foreach dir,$(cursubdirs), \
|
||||
$(call includemakefile,$(dir))) \
|
||||
$(if $(subdirs), \
|
||||
$(call evaluate_subdirs))
|
||||
|
||||
# collect all object files eligible for building
|
||||
subdirs := .
|
||||
$(call evaluate_subdirs)
|
||||
|
||||
# Eliminate duplicate mentions of source files
|
||||
$(name)-srcs := $(sort $($(name)-srcs))
|
||||
$(name)-gens := $(sort $($(name)-gens))
|
||||
|
||||
# For Ada includes
|
||||
$(name)-ada-dirs := $(sort $(dir $(filter %.ads %.adb,$($(name)-srcs) $($(name)-gens))))
|
||||
|
||||
# To track dependencies, we need all Ada specification (.ads) files in
|
||||
# *-srcs. Extract / filter all specification files that have a matching
|
||||
# body (.adb) file here (specifications without a body are valid sources
|
||||
# in Ada).
|
||||
$(name)-extra-specs := \
|
||||
$(filter \
|
||||
$(addprefix %/,$(patsubst %.adb,%.ads,$(notdir $(filter %.adb,$($(name)-srcs))))), \
|
||||
$(filter %.ads,$($(name)-srcs) $($(name)-gens)))
|
||||
$(name)-srcs := $(filter-out $($(name)-extra-specs),$($(name)-srcs))
|
||||
$(name)-gens := $(filter-out $($(name)-extra-specs),$($(name)-gens))
|
||||
|
||||
$(name)-objs := $(call src-to-obj,,$($(name)-srcs) $($(name)-gens))
|
||||
$(name)-alis := $(call src-to-ali,,$($(name)-srcs) $($(name)-gens))
|
||||
|
||||
# For gnatprove
|
||||
$(name)-proof-dirs := \
|
||||
$(sort $(dir $($(name)-proof)) \
|
||||
$(filter-out ada/% %/ada/%,$($(name)-ada-dirs)))
|
||||
|
||||
# For mkdir
|
||||
alldirs := $(abspath $(dir $(sort $($(name)-objs))))
|
||||
|
||||
# Reads dependencies from an Ada library information (.ali) file
|
||||
# Only basenames (with suffix) are preserved so we have to look the
|
||||
# paths up in $($(name)-srcs) $($(name)-gens).
|
||||
# $1 ali file
|
||||
create_ada_deps = \
|
||||
$(if $(wildcard $(1)),\
|
||||
$(filter \
|
||||
$(addprefix %/,$(shell sed -ne's/^D \([^\t]\+\).*$$/\1/p' $(1) 2>/dev/null)), \
|
||||
$($(name)-srcs) $($(name)-gens) $($(name)-extra-specs)), \
|
||||
$($(name)-gens))
|
||||
|
||||
# Adds dependency rules
|
||||
# $1 source file
|
||||
add_ada_deps = \
|
||||
$(call src-to-obj,,$(1)): $(1) \
|
||||
$(call create_ada_deps,$(call src-to-ali,,$(1)))
|
||||
|
||||
# Writes a compilation rule for a source type
|
||||
# $1 source type (ads, adb)
|
||||
# $2 source files (including the colon)
|
||||
# $3 obj path prefix (including the trailing slash)
|
||||
define add_ada_rule
|
||||
$(2) $(3)%.o: %.$(1)
|
||||
@printf " COMPILE $$(subst $(obj)/,,$$@)\n"
|
||||
$(CC) \
|
||||
$(ADAFLAGS) $(addprefix -I,$($(name)-ada-dirs) $($(name)-extra-incs)) \
|
||||
-c -o $$@ $$<
|
||||
endef
|
||||
|
||||
# For sources
|
||||
$(foreach type,ads adb, \
|
||||
$(eval $(call add_ada_rule,$(type),$(call src-to-obj,,$(filter %.$(type),$($(name)-srcs))):,$(obj)/)))
|
||||
$(foreach file,$($(name)-srcs) $($(name)-gens), \
|
||||
$(eval $(call add_ada_deps,$(file))))
|
||||
|
||||
# For generated sources already in $(obj)/
|
||||
$(foreach type,ads adb, \
|
||||
$(eval $(call add_ada_rule,$(type),$(call src-to-obj,,$(filter %.$(type),$($(name)-gens))):,)))
|
||||
|
||||
# Ali files are generated along with the object file. They need an empty
|
||||
# recipe for correct updating.
|
||||
$($(name)-alis): %.ali: %.o ;
|
||||
|
||||
# To support complex package initializations, we need to call the
|
||||
# emitted code explicitly. gnatbind gathers all the calls for us
|
||||
# and exports them as a procedure $(name)_adainit(). Every stage that
|
||||
# uses Ada code has to call it!
|
||||
$(obj)/b__lib$(name).adb: $($(name)-alis)
|
||||
@printf " BIND $(subst $(obj)/,,$@)\n"
|
||||
# We have to give gnatbind a simple filename (without leading
|
||||
# path components) so just cd there.
|
||||
cd $(dir $@) && \
|
||||
$(GNATBIND) $(addprefix -aO,$(abspath $($(name)-extra-objs))) \
|
||||
-a -n -L$(name)_ada -o $(notdir $@) \
|
||||
$(subst $(dir $@),,$^)
|
||||
$(eval $(call add_ada_rule,adb,$(obj)/b__lib$(name).o:,))
|
||||
$(name)-objs += $(obj)/b__lib$(name).o
|
||||
|
||||
$(shell mkdir -p $(alldirs))
|
||||
|
||||
$(name)-install-srcs = $(sort \
|
||||
$($(name)-extra-specs) $(filter %.ads,$($(name)-srcs)) \
|
||||
$(foreach adb,$(filter %.adb,$($(name)-srcs)), \
|
||||
$(shell grep -q '^U .*\<BN\>' $(call src-to-ali,,$(adb)) 2>/dev/null && echo $(adb))))
|
||||
|
||||
$(name)-install-proof = \
|
||||
$(filter $(addprefix %/,$(notdir $($(name)-install-srcs))),$($(name)-proof)) \
|
||||
$(filter-out $(addprefix %/,$(notdir $($(name)-proof))),$($(name)-install-srcs))
|
||||
|
||||
install: $(binary) $($(name)-alis) $(libgpr)
|
||||
install -d $(DESTDIR)/lib $(DESTDIR)/include $(DESTDIR)/proof
|
||||
printf " INSTALL $(subst $(obj)/,,$(binary))\n"
|
||||
install $(binary) $(DESTDIR)/lib/
|
||||
$(foreach file,$($(name)-install) $(libgpr), \
|
||||
printf " INSTALL $(subst $(obj)/,,$(file))\n"; \
|
||||
install $(file) $(DESTDIR);)
|
||||
printf " INSTALL $(cnf)\n"
|
||||
install $(cnf) $(DESTDIR)/config
|
||||
printf " INSTALL %s\n" $(subst $(obj)/,,$($(name)-alis))
|
||||
install $($(name)-alis) $(DESTDIR)/lib/
|
||||
printf " INSTALL %s\n" $(subst $(obj)/,,$($(name)-install-srcs))
|
||||
install $($(name)-install-srcs) $(DESTDIR)/include/
|
||||
printf " INSTALL %s\n" $(subst $(obj)/,,$($(name)-install-proof))
|
||||
install $($(name)-install-proof) $(DESTDIR)/proof/
|
||||
|
||||
clean::
|
||||
rm -rf $(obj) $(name).gpr
|
||||
|
||||
distclean: clean
|
||||
rm -rf dest
|
||||
|
||||
.PHONY: install clean distclean
|
|
@ -0,0 +1,2 @@
|
|||
subdirs-y += ada common proof
|
||||
subdirs-y += debug
|
|
@ -0,0 +1,97 @@
|
|||
PROOF_MODE ?= all
|
||||
|
||||
jobs ?= 4
|
||||
|
||||
$(foreach dep,$($(name)-deplibs), \
|
||||
$(eval SPARKFLAGS += -aP=$($(dep)-dir)))
|
||||
|
||||
SPARKFLAGS += -j$(jobs)
|
||||
SPARKFLAGS += -k
|
||||
SPARKFLAGS += -m
|
||||
SPARKFLAGS += --mode=$(PROOF_MODE)
|
||||
SPARKFLAGS += --report=fail
|
||||
SPARKFLAGS += --warnings=error
|
||||
SPARKFLAGS += --prover=cvc4,z3 --steps=500 --timeout=1 # FIXME: timeout used because steps seems broken
|
||||
|
||||
quote-list = $(subst $(space),$(comma),$(patsubst %,"%",$(1)))
|
||||
|
||||
$(name)-exclude-srcs = \
|
||||
$(filter-out \
|
||||
$(sort $(notdir $($(name)-proof) $($(name)-srcs) $($(name)-gens) $($(name)-extra-specs))), \
|
||||
$(sort $(notdir \
|
||||
$(wildcard $(addsuffix *.ad[sb],$($(name)-proof-dirs))))))
|
||||
|
||||
# Has to reside in the working directory. gnatprove takes paths relative
|
||||
# to the directory wher it's placed and reports internal errors if used
|
||||
# with absolute paths.
|
||||
gpr := $(name).gpr
|
||||
gpr-name = $(subst -,_,$(subst .,_,$(basename $(notdir $@))))
|
||||
|
||||
# Will be installed for inclusion
|
||||
libgpr := $(obj)/lib$(name).gpr
|
||||
|
||||
.SECONDEXPANSION:
|
||||
|
||||
$(gpr):
|
||||
@printf " GENERATE $(subst $(obj)/,,$@)\n"
|
||||
printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
|
||||
echo 'library project $(gpr-name) is' >>$@
|
||||
echo ' for Library_Name use "$(name)";' >>$@
|
||||
echo ' for Library_Dir use "$(obj)/adalib";' >>$@
|
||||
echo ' for Source_Dirs use' \
|
||||
'($(call quote-list,$($(name)-proof-dirs)));' >>$@
|
||||
echo ' for Object_Dir use "$(obj)";' >>$@
|
||||
echo ' package Builder is' >>$@
|
||||
echo ' for Global_Configuration_Pragmas use' \
|
||||
'"$(abspath $(libhw-dir)/spark.adc)";' >>$@
|
||||
echo ' end Builder;' >>$@
|
||||
echo ' for Excluded_Source_Files use' \
|
||||
'($(call quote-list,$($(name)-exclude-srcs)));' >>$@
|
||||
echo 'end $(gpr-name);' >>$@
|
||||
|
||||
.INTERMEDIATE: $(gpr)
|
||||
|
||||
$(libgpr): $$(MAKEFILE_LIST)
|
||||
@printf " GENERATE $(subst $(obj)/,,$@)\n"
|
||||
printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
|
||||
echo 'library project lib$(name) is' >>$@
|
||||
echo ' for Library_Name use "$(name)";' >>$@
|
||||
echo ' for Library_Dir use "lib";' >>$@
|
||||
echo ' for Library_ALI_Dir use "lib";' >>$@
|
||||
echo ' for Source_Dirs use ("proof");' >>$@
|
||||
echo ' for Object_Dir use external ("obj", "build");' >>$@
|
||||
echo 'end lib$(name);' >>$@
|
||||
|
||||
$(obj)/gnatprove/gnatprove.out: $(gpr) $$($(name)-gens) $(obj)/proofmode
|
||||
gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj))
|
||||
|
||||
proof:
|
||||
if [ "$(PROOF_MODE)" != "$$(cat $(obj)/proofmode 2>/dev/null)" ]; then \
|
||||
echo "$(PROOF_MODE)" >$(obj)/proofmode; \
|
||||
fi
|
||||
$(MAKE) $(obj)/gnatprove/gnatprove.out
|
||||
|
||||
check: export override PROOF_MODE=check
|
||||
check: proof
|
||||
|
||||
flow: export override PROOF_MODE=flow
|
||||
flow: proof
|
||||
|
||||
full: export override PROOF_MODE=all
|
||||
full: proof
|
||||
|
||||
allconfigs = $(wildcard configs/*)
|
||||
allconfigs-targets = $(addprefix allconfigs-,$(notdir $(allconfigs)))
|
||||
|
||||
$(allconfigs-targets): allconfigs-%: configs/%
|
||||
rm -rf proof-allconfigs/$* $(name)_$*.gpr
|
||||
mkdir -p proof-allconfigs/$*
|
||||
echo "$(PROOF_MODE)" >proof-allconfigs/$*/proofmode
|
||||
$(MAKE) obj=proof-allconfigs/$* cnf=configs/$* gpr=$(name)_$*.gpr jobs=1 proof-allconfigs/$*/gnatprove/gnatprove.out
|
||||
|
||||
proof-allconfigs: $(allconfigs-targets)
|
||||
|
||||
clean::
|
||||
rm -rf proof-allconfigs/
|
||||
|
||||
.PHONY: proof check flow full $(allconfigs-targets) proof-allconfigs
|
|
@ -0,0 +1,3 @@
|
|||
hw-$(CONFIG_HWBASE_STATIC_MMIO) += static_mmio/hw-mmio_range.adb
|
||||
hw-$(CONFIG_HWBASE_DYNAMIC_MMIO) += dynamic_mmio/hw-mmio_range.adb
|
||||
hw-$(CONFIG_HWBASE_TIMER_CLOCK_GETTIME) += clock_gettime/hw-time-timer.adb
|
|
@ -0,0 +1,61 @@
|
|||
--
|
||||
-- Copyright (C) 2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with Interfaces.C;
|
||||
|
||||
use type Interfaces.C.long;
|
||||
|
||||
package body HW.Time.Timer
|
||||
with
|
||||
Refined_State => (Timer_State => null,
|
||||
Abstract_Time => null)
|
||||
is
|
||||
CLOCK_MONOTONIC_RAW : constant := 4;
|
||||
|
||||
subtype Clock_ID_T is Interfaces.C.int;
|
||||
subtype Time_T is Interfaces.C.long;
|
||||
|
||||
type Struct_Timespec is record
|
||||
TV_Sec : aliased Time_T;
|
||||
TV_NSec : aliased Interfaces.C.long;
|
||||
end record;
|
||||
pragma Convention (C_Pass_By_Copy, Struct_Timespec);
|
||||
|
||||
function Clock_Gettime
|
||||
(Clock_ID : Clock_ID_T;
|
||||
Timespec : access Struct_Timespec)
|
||||
return Interfaces.C.int;
|
||||
pragma Import (C, Clock_Gettime, "clock_gettime");
|
||||
|
||||
function Raw_Value_Min return T
|
||||
is
|
||||
Ignored : Interfaces.C.int;
|
||||
Timespec : aliased Struct_Timespec;
|
||||
begin
|
||||
Ignored := Clock_Gettime (CLOCK_MONOTONIC_RAW, Timespec'Access);
|
||||
return T (Timespec.TV_Sec * 1_000_000_000 + Timespec.TV_NSec);
|
||||
end Raw_Value_Min;
|
||||
|
||||
function Raw_Value_Max return T
|
||||
is
|
||||
begin
|
||||
return Raw_Value_Min + 1;
|
||||
end Raw_Value_Max;
|
||||
|
||||
function Hz return T
|
||||
is
|
||||
begin
|
||||
return 1_000_000_000; -- clock_gettime(2) is fixed to nanoseconds
|
||||
end Hz;
|
||||
|
||||
end HW.Time.Timer;
|
|
@ -0,0 +1,76 @@
|
|||
--
|
||||
-- Copyright (C) 2015-2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with HW.Debug;
|
||||
with GNAT.Source_Info;
|
||||
with System.Storage_Elements;
|
||||
with System.Address_To_Access_Conversions;
|
||||
|
||||
package body HW.MMIO_Range
|
||||
with
|
||||
Refined_State =>
|
||||
(State => Range_A, -- the contents accessed
|
||||
Base_Address => null) -- the address, so actually Range_A too
|
||||
is
|
||||
pragma Warnings (Off, "implicit dereference",
|
||||
Reason => "This is what this package is about.");
|
||||
|
||||
Debug_Reads : constant Boolean := False;
|
||||
Debug_Writes : constant Boolean := False;
|
||||
|
||||
type Range_Access is access all Array_T;
|
||||
package Conv_Range is new System.Address_To_Access_Conversions (Array_T);
|
||||
|
||||
Range_A : Range_Access :=
|
||||
Range_Access (Conv_Range.To_Pointer (System'To_Address (Base_Addr)))
|
||||
with Volatile;
|
||||
|
||||
procedure Read (Value : out Element_T; Index : in Index_T)
|
||||
is
|
||||
use type Word32;
|
||||
begin
|
||||
Value := Range_A (Index);
|
||||
pragma Debug (Debug_Reads, Debug.Put
|
||||
(GNAT.Source_Info.Enclosing_Entity & ": "));
|
||||
pragma Debug (Debug_Reads, Debug.Put_Word32 (Word32 (Value)));
|
||||
pragma Debug (Debug_Reads, Debug.Put (" <- "));
|
||||
pragma Debug (Debug_Reads, Debug.Put_Word32
|
||||
(Word32 (System.Storage_Elements.To_Integer
|
||||
(Conv_Range.To_Address (Conv_Range.Object_Pointer (Range_A)))) +
|
||||
Word32 (Index) * (Element_T'Size / 8)));
|
||||
pragma Debug (Debug_Reads, Debug.New_Line);
|
||||
end Read;
|
||||
|
||||
procedure Write (Index : in Index_T; Value : in Element_T)
|
||||
is
|
||||
use type Word32;
|
||||
begin
|
||||
pragma Debug (Debug_Writes, Debug.Put
|
||||
(GNAT.Source_Info.Enclosing_Entity & ": "));
|
||||
pragma Debug (Debug_Writes, Debug.Put_Word32 (Word32 (Value)));
|
||||
pragma Debug (Debug_Writes, Debug.Put (" -> "));
|
||||
pragma Debug (Debug_Writes, Debug.Put_Word32
|
||||
(Word32 (System.Storage_Elements.To_Integer
|
||||
(Conv_Range.To_Address (Conv_Range.Object_Pointer (Range_A)))) +
|
||||
Word32 (Index) * (Element_T'Size / 8)));
|
||||
pragma Debug (Debug_Writes, Debug.New_Line);
|
||||
Range_A (Index) := Value;
|
||||
end Write;
|
||||
|
||||
procedure Set_Base_Address (Base : Word64) is
|
||||
begin
|
||||
Range_A := Range_Access
|
||||
(Conv_Range.To_Pointer (System'To_Address (Base)));
|
||||
end Set_Base_Address;
|
||||
|
||||
end HW.MMIO_Range;
|
|
@ -0,0 +1,35 @@
|
|||
--
|
||||
-- Copyright (C) 2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
package body HW.MMIO_Range
|
||||
with
|
||||
Refined_State =>
|
||||
(State => MMIO,
|
||||
Base_Address => null)
|
||||
is
|
||||
|
||||
MMIO : Array_T with Volatile, Address => System'To_Address (Base_Addr);
|
||||
|
||||
procedure Read (Value : out Element_T; Index : in Index_T) is
|
||||
begin
|
||||
Value := MMIO (Index);
|
||||
end Read;
|
||||
|
||||
procedure Write (Index : in Index_T; Value : in Element_T) is
|
||||
begin
|
||||
MMIO (Index) := Value;
|
||||
end Write;
|
||||
|
||||
procedure Set_Base_Address (Base : Word64) is null;
|
||||
|
||||
end HW.MMIO_Range;
|
|
@ -0,0 +1,10 @@
|
|||
hw-y += hw.ads
|
||||
hw-y += hw-mmio_range.ads
|
||||
hw-y += hw-mmio_regs.adb
|
||||
hw-y += hw-mmio_regs.ads
|
||||
hw-y += hw-port_io.adb
|
||||
hw-y += hw-port_io.ads
|
||||
hw-y += hw-sub_regs.ads
|
||||
hw-y += hw-time.ads
|
||||
hw-y += hw-time.adb
|
||||
hw-y += hw-time-timer.ads
|
|
@ -0,0 +1,35 @@
|
|||
--
|
||||
-- Copyright (C) 2015-2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with System;
|
||||
|
||||
generic
|
||||
Base_Addr : Word64;
|
||||
type Element_T is mod <>;
|
||||
type Index_T is range <>;
|
||||
type Array_T is array (Index_T) of Element_T;
|
||||
package HW.MMIO_Range
|
||||
with
|
||||
Abstract_State =>
|
||||
((State with External),
|
||||
Base_Address),
|
||||
Initializes => Base_Address
|
||||
is
|
||||
|
||||
procedure Read (Value : out Element_T; Index : in Index_T);
|
||||
|
||||
procedure Write (Index : in Index_T; Value : in Element_T);
|
||||
|
||||
procedure Set_Base_Address (Base : Word64);
|
||||
|
||||
end HW.MMIO_Range;
|
|
@ -0,0 +1,92 @@
|
|||
--
|
||||
-- Copyright (C) 2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
package body HW.MMIO_Regs
|
||||
is
|
||||
|
||||
generic
|
||||
type Word_T is mod <>;
|
||||
procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T);
|
||||
|
||||
procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T)
|
||||
is
|
||||
Off : constant Range_P.Index_T := Range_P.Index_T
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
|
||||
pragma Warnings
|
||||
(GNAT, Off, """Mask"" is not modified, could be declared constant",
|
||||
Reason => "Ada RM forbids making it constant.");
|
||||
Mask : Word64 := Shift_Left (1, Regs (Idx).MSB + 1 - Regs (Idx).LSB) - 1;
|
||||
pragma Warnings
|
||||
(GNAT, On, """Mask"" is not modified, could be declared constant");
|
||||
Temp : Range_P.Element_T;
|
||||
begin
|
||||
Range_P.Read (Temp, Off);
|
||||
Value := Word_T (Shift_Right (Word64 (Temp), Regs (Idx).LSB) and Mask);
|
||||
end Read_G;
|
||||
|
||||
procedure Read_I is new Read_G (Word8);
|
||||
procedure Read (Value : out Word8; Idx : Subs_P.Index_T) renames Read_I;
|
||||
|
||||
procedure Read_I is new Read_G (Word16);
|
||||
procedure Read (Value : out Word16; Idx : Subs_P.Index_T) renames Read_I;
|
||||
|
||||
procedure Read_I is new Read_G (Word32);
|
||||
procedure Read (Value : out Word32; Idx : Subs_P.Index_T) renames Read_I;
|
||||
|
||||
procedure Read_I is new Read_G (Word64);
|
||||
procedure Read (Value : out Word64; Idx : Subs_P.Index_T) renames Read_I;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
generic
|
||||
type Word_T is mod <>;
|
||||
procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T);
|
||||
|
||||
procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T)
|
||||
is
|
||||
Off : constant Range_P.Index_T := Range_P.Index_T
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
|
||||
pragma Warnings
|
||||
(GNAT, Off, """Mask"" is not modified, could be declared constant",
|
||||
Reason => "Ada RM forbids making it constant.");
|
||||
Mask : Word64 :=
|
||||
Shift_Left (1, Regs (Idx).MSB + 1) - Shift_Left (1, Regs (Idx).LSB);
|
||||
pragma Warnings
|
||||
(GNAT, On, """Mask"" is not modified, could be declared constant");
|
||||
Temp : Range_P.Element_T;
|
||||
begin
|
||||
if Regs (Idx).MSB - Regs (Idx).LSB + 1 = Range_P.Element_T'Size then
|
||||
Range_P.Write (Off, Range_P.Element_T (Value));
|
||||
else
|
||||
-- read/modify/write
|
||||
Range_P.Read (Temp, Off);
|
||||
Temp := Range_P.Element_T
|
||||
((Word64 (Temp) and not Mask) or
|
||||
(Shift_Left (Word64 (Value), Regs (Idx).LSB)));
|
||||
Range_P.Write (Off, Temp);
|
||||
end if;
|
||||
end Write_G;
|
||||
|
||||
procedure Write_I is new Write_G (Word8);
|
||||
procedure Write (Idx : Subs_P.Index_T; Value : Word8) renames Write_I;
|
||||
|
||||
procedure Write_I is new Write_G (Word16);
|
||||
procedure Write (Idx : Subs_P.Index_T; Value : Word16) renames Write_I;
|
||||
|
||||
procedure Write_I is new Write_G (Word32);
|
||||
procedure Write (Idx : Subs_P.Index_T; Value : Word32) renames Write_I;
|
||||
|
||||
procedure Write_I is new Write_G (Word64);
|
||||
procedure Write (Idx : Subs_P.Index_T; Value : Word64) renames Write_I;
|
||||
|
||||
end HW.MMIO_Regs;
|
|
@ -0,0 +1,127 @@
|
|||
--
|
||||
-- Copyright (C) 2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with HW.Sub_Regs;
|
||||
with HW.MMIO_Range;
|
||||
|
||||
use type HW.Word64;
|
||||
|
||||
generic
|
||||
with package Range_P is new MMIO_Range (<>);
|
||||
Byte_Offset_O : Natural := 0;
|
||||
|
||||
with package Subs_P is new Sub_Regs (<>);
|
||||
Regs : Subs_P.Array_T;
|
||||
|
||||
package HW.MMIO_Regs
|
||||
is
|
||||
|
||||
Byte_Offset : Natural := Byte_Offset_O;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Read (Value : out Word8; Idx : Subs_P.Index_T)
|
||||
with
|
||||
Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
|
||||
Range_P.Element_T'Size <= Word64'Size and
|
||||
Regs (Idx).MSB < Range_P.Element_T'Size and
|
||||
Regs (Idx).MSB >= Regs (Idx).LSB and
|
||||
Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word8'Size;
|
||||
|
||||
procedure Read (Value : out Word16; Idx : Subs_P.Index_T)
|
||||
with
|
||||
Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
|
||||
Range_P.Element_T'Size <= Word64'Size and
|
||||
Regs (Idx).MSB < Range_P.Element_T'Size and
|
||||
Regs (Idx).MSB >= Regs (Idx).LSB and
|
||||
Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word16'Size;
|
||||
|
||||
procedure Read (Value : out Word32; Idx : Subs_P.Index_T)
|
||||
with
|
||||
Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
|
||||
Range_P.Element_T'Size <= Word64'Size and
|
||||
Regs (Idx).MSB < Range_P.Element_T'Size and
|
||||
Regs (Idx).MSB >= Regs (Idx).LSB and
|
||||
Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word32'Size;
|
||||
|
||||
procedure Read (Value : out Word64; Idx : Subs_P.Index_T)
|
||||
with
|
||||
Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
|
||||
Range_P.Element_T'Size <= Word64'Size and
|
||||
Regs (Idx).MSB < Range_P.Element_T'Size and
|
||||
Regs (Idx).MSB >= Regs (Idx).LSB and
|
||||
Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word64'Size;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Write (Idx : Subs_P.Index_T; Value : Word8)
|
||||
with
|
||||
Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
|
||||
Range_P.Element_T'Size <= Word64'Size and
|
||||
Regs (Idx).MSB < Range_P.Element_T'Size and
|
||||
Regs (Idx).MSB >= Regs (Idx).LSB and
|
||||
Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
|
||||
Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
|
||||
|
||||
procedure Write (Idx : Subs_P.Index_T; Value : Word16)
|
||||
with
|
||||
Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
|
||||
Range_P.Element_T'Size <= Word64'Size and
|
||||
Regs (Idx).MSB < Range_P.Element_T'Size and
|
||||
Regs (Idx).MSB >= Regs (Idx).LSB and
|
||||
Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
|
||||
Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
|
||||
|
||||
procedure Write (Idx : Subs_P.Index_T; Value : Word32)
|
||||
with
|
||||
Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
|
||||
Range_P.Element_T'Size <= Word64'Size and
|
||||
Regs (Idx).MSB < Range_P.Element_T'Size and
|
||||
Regs (Idx).MSB >= Regs (Idx).LSB and
|
||||
Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
|
||||
Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
|
||||
|
||||
procedure Write (Idx : Subs_P.Index_T; Value : Word64)
|
||||
with
|
||||
Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
|
||||
((Byte_Offset + Regs (Idx).Byte_Offset) /
|
||||
(Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
|
||||
Range_P.Element_T'Size <= Word64'Size and
|
||||
Regs (Idx).MSB < Range_P.Element_T'Size and
|
||||
Regs (Idx).MSB >= Regs (Idx).LSB and
|
||||
Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
|
||||
Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
|
||||
|
||||
end HW.MMIO_Regs;
|
|
@ -0,0 +1,71 @@
|
|||
--
|
||||
-- Copyright (C) 2015 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with System;
|
||||
with System.Machine_Code;
|
||||
|
||||
package body HW.Port_IO
|
||||
with
|
||||
Refined_State => (State => null),
|
||||
SPARK_Mode => Off
|
||||
is
|
||||
|
||||
generic
|
||||
type Word is private;
|
||||
procedure Port_In (Value : out Word; Port : Port_Type);
|
||||
|
||||
procedure Port_In (Value : out Word; Port : Port_Type) is
|
||||
begin
|
||||
System.Machine_Code.Asm
|
||||
("in %1, %0",
|
||||
Inputs => (Port_Type'Asm_Input ("Nd", Port)),
|
||||
Outputs => (Word'Asm_Output ("=a", Value)),
|
||||
Volatile => True);
|
||||
end Port_In;
|
||||
|
||||
procedure InB_Body is new Port_In (Word => Word8);
|
||||
procedure InB (Value : out Word8; Port : Port_Type) renames InB_Body;
|
||||
|
||||
procedure InW_Body is new Port_In (Word => Word16);
|
||||
procedure InW (Value : out Word16; Port : Port_Type) renames InW_Body;
|
||||
|
||||
procedure InL_Body is new Port_In (Word => Word32);
|
||||
procedure InL (Value : out Word32; Port : Port_Type) renames InL_Body;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
generic
|
||||
type Word is private;
|
||||
procedure Port_Out (Port : Port_Type; Value : Word);
|
||||
|
||||
procedure Port_Out (Port : Port_Type; Value : Word) is
|
||||
begin
|
||||
System.Machine_Code.Asm
|
||||
("out %1, %0",
|
||||
Inputs => (Port_Type'Asm_Input ("Nd", Port),
|
||||
Word'Asm_Input ("a", Value)),
|
||||
Volatile => True);
|
||||
end Port_Out;
|
||||
|
||||
procedure OutB_Body is new Port_Out (Word => Word8);
|
||||
procedure OutB (Port : Port_Type; Value : Word8) renames OutB_Body;
|
||||
|
||||
procedure OutW_Body is new Port_Out (Word => Word16);
|
||||
procedure OutW (Port : Port_Type; Value : Word16) renames OutW_Body;
|
||||
|
||||
procedure OutL_Body is new Port_Out (Word => Word32);
|
||||
procedure OutL (Port : Port_Type; Value : Word32) renames OutL_Body;
|
||||
|
||||
end HW.Port_IO;
|
||||
|
||||
-- vim: set ts=8 sts=3 sw=3 et:
|
|
@ -0,0 +1,61 @@
|
|||
--
|
||||
-- Copyright (C) 2015 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
package HW.Port_IO
|
||||
with
|
||||
Abstract_State => (State with External => (Async_Readers, Async_Writers))
|
||||
is
|
||||
|
||||
type Port_Type is mod 2**16;
|
||||
|
||||
procedure InB (Value : out Word8; Port : Port_Type)
|
||||
with
|
||||
Global => (In_Out => State),
|
||||
Depends => ((Value, State) => (Port, State)),
|
||||
Inline_Always;
|
||||
|
||||
procedure InW (Value : out Word16; Port : Port_Type)
|
||||
with
|
||||
Global => (In_Out => State),
|
||||
Depends => ((Value, State) => (Port, State)),
|
||||
Pre => Port mod 2 = 0,
|
||||
Inline_Always;
|
||||
|
||||
procedure InL (Value : out Word32; Port : Port_Type)
|
||||
with
|
||||
Global => (In_Out => State),
|
||||
Depends => ((Value, State) => (Port, State)),
|
||||
Pre => Port mod 4 = 0,
|
||||
Inline_Always;
|
||||
|
||||
procedure OutB (Port : Port_Type; Value : Word8)
|
||||
with
|
||||
Global => (In_Out => State),
|
||||
Depends => (State =>+ (Port, Value)),
|
||||
Inline_Always;
|
||||
|
||||
procedure OutW (Port : Port_Type; Value : Word16)
|
||||
with
|
||||
Global => (In_Out => State),
|
||||
Depends => (State =>+ (Port, Value)),
|
||||
Pre => Port mod 2 = 0,
|
||||
Inline_Always;
|
||||
|
||||
procedure OutL (Port : Port_Type; Value : Word32)
|
||||
with
|
||||
Global => (In_Out => State),
|
||||
Depends => (State =>+ (Port, Value)),
|
||||
Pre => Port mod 4 = 0,
|
||||
Inline_Always;
|
||||
|
||||
end HW.Port_IO;
|
|
@ -0,0 +1,26 @@
|
|||
--
|
||||
-- Copyright (C) 2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
generic
|
||||
type Index_T is (<>);
|
||||
package HW.Sub_Regs is
|
||||
|
||||
type T is record
|
||||
Byte_Offset : Natural;
|
||||
MSB : Natural;
|
||||
LSB : Natural;
|
||||
end record;
|
||||
|
||||
type Array_T is array (Index_T) of T;
|
||||
|
||||
end HW.Sub_Regs;
|
|
@ -0,0 +1,41 @@
|
|||
--
|
||||
-- Copyright (C) 2015-2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
private package HW.Time.Timer
|
||||
with
|
||||
Abstract_State => ((Timer_State with Part_Of => HW.Time.State),
|
||||
(Abstract_Time with
|
||||
Part_Of => HW.Time.State,
|
||||
External => Async_Writers)),
|
||||
Initializes => (Timer_State)
|
||||
is
|
||||
|
||||
-- Returns the highest point in time that has definitely passed.
|
||||
function Raw_Value_Min return T
|
||||
with
|
||||
Volatile_Function,
|
||||
Global => (Input => Abstract_Time),
|
||||
Depends => (Raw_Value_Min'Result => Abstract_Time);
|
||||
|
||||
-- Returns the highest point in time that might have been reached yet.
|
||||
function Raw_Value_Max return T
|
||||
with
|
||||
Volatile_Function,
|
||||
Global => (Input => Abstract_Time),
|
||||
Depends => (Raw_Value_Max'Result => Abstract_Time);
|
||||
|
||||
function Hz return T
|
||||
with
|
||||
Global => (Input => Timer_State);
|
||||
|
||||
end HW.Time.Timer;
|
|
@ -0,0 +1,105 @@
|
|||
--
|
||||
-- Copyright (C) 2015-2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with HW;
|
||||
with HW.Time.Timer;
|
||||
|
||||
use type HW.Word64;
|
||||
|
||||
package body HW.Time
|
||||
with Refined_State => (State => (Timer.Timer_State, Timer.Abstract_Time))
|
||||
is
|
||||
|
||||
function Now return T
|
||||
with
|
||||
Refined_Global => (Input => Timer.Abstract_Time)
|
||||
is
|
||||
Current : constant T := Timer.Raw_Value_Min;
|
||||
begin
|
||||
return Current;
|
||||
end Now;
|
||||
|
||||
function US_From_Now (US : Natural) return T
|
||||
with
|
||||
Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
|
||||
is
|
||||
Current : constant T := Timer.Raw_Value_Max;
|
||||
begin
|
||||
return Current + (T (US) * Timer.Hz + 999_999) / 1_000_000;
|
||||
end US_From_Now;
|
||||
|
||||
function MS_From_Now (MS : Natural) return T
|
||||
with
|
||||
Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
|
||||
is
|
||||
Current : constant T := Timer.Raw_Value_Max;
|
||||
begin
|
||||
return Current + (T (MS) * Timer.Hz + 999) / 1_000;
|
||||
end MS_From_Now;
|
||||
|
||||
function Now_US return Int64
|
||||
with
|
||||
Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
|
||||
is
|
||||
MHz : constant T := Timer.Hz / 1_000_000;
|
||||
Current : constant T := Timer.Raw_Value_Min;
|
||||
begin
|
||||
return Int64 ((Current and (2 ** 63 - 1)) / (if MHz = 0 then 1 else MHz));
|
||||
end Now_US;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Delay_Until (Deadline : T)
|
||||
with
|
||||
Refined_Global => (Input => (Timer.Abstract_Time))
|
||||
is
|
||||
Current: T;
|
||||
begin
|
||||
loop
|
||||
Current := Timer.Raw_Value_Min;
|
||||
exit when Current >= Deadline;
|
||||
end loop;
|
||||
end Delay_Until;
|
||||
|
||||
procedure U_Delay (US : Natural)
|
||||
with
|
||||
Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
|
||||
is
|
||||
Deadline : constant T := US_From_Now (US);
|
||||
begin
|
||||
Delay_Until (Deadline);
|
||||
end U_Delay;
|
||||
|
||||
procedure M_Delay (MS : Natural)
|
||||
with
|
||||
Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
|
||||
is
|
||||
Deadline : constant T := MS_From_Now (MS);
|
||||
begin
|
||||
Delay_Until (Deadline);
|
||||
end M_Delay;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
function Timed_Out (Deadline : T) return Boolean
|
||||
with
|
||||
Refined_Global => (Input => (Timer.Abstract_Time))
|
||||
is
|
||||
Current : constant T := Timer.Raw_Value_Min;
|
||||
begin
|
||||
return Current >= Deadline;
|
||||
end Timed_Out;
|
||||
|
||||
end HW.Time;
|
||||
|
||||
-- vim: set ts=8 sts=3 sw=3 et:
|
|
@ -0,0 +1,75 @@
|
|||
--
|
||||
-- Copyright (C) 2015-2016 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
package HW.Time
|
||||
with Abstract_State => (State with External => Async_Writers)
|
||||
is
|
||||
|
||||
type T is private;
|
||||
|
||||
function Now return T
|
||||
with
|
||||
Volatile_Function,
|
||||
Global => (Input => State);
|
||||
|
||||
function US_From_Now (US : Natural) return T
|
||||
with
|
||||
Volatile_Function,
|
||||
Global => (Input => State);
|
||||
|
||||
function MS_From_Now (MS : Natural) return T
|
||||
with
|
||||
Volatile_Function,
|
||||
Global => (Input => State);
|
||||
|
||||
function Now_US return Int64
|
||||
with
|
||||
Volatile_Function,
|
||||
Global => (Input => State);
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
pragma Warnings
|
||||
(GNATprove, Off, "subprogram ""*Delay*"" has no effect",
|
||||
Reason => "No effect on dataflow but time always passes.");
|
||||
|
||||
-- Delay execution until Deadline has been reached.
|
||||
procedure Delay_Until (Deadline : T)
|
||||
with
|
||||
Global => (Input => State);
|
||||
|
||||
procedure U_Delay (US : Natural)
|
||||
with
|
||||
Global => (Input => State);
|
||||
|
||||
procedure M_Delay (MS : Natural)
|
||||
with
|
||||
Global => (Input => State);
|
||||
|
||||
pragma Warnings
|
||||
(GNATprove, On, "subprogram ""*Delay*"" has no effect");
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
function Timed_Out (Deadline : T) return Boolean
|
||||
with
|
||||
Volatile_Function,
|
||||
Global => (Input => State);
|
||||
|
||||
private
|
||||
|
||||
type T is new Word64;
|
||||
|
||||
end HW.Time;
|
||||
|
||||
-- vim: set ts=8 sts=3 sw=3 et:
|
|
@ -0,0 +1,58 @@
|
|||
--
|
||||
-- Copyright (C) 2015 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with Interfaces;
|
||||
|
||||
package HW is
|
||||
|
||||
type Bit is mod 2 ** 1;
|
||||
|
||||
subtype Byte is Interfaces.Unsigned_8;
|
||||
subtype Word8 is Byte;
|
||||
function Shift_Left (Value : Word8; Amount : Natural) return Word8
|
||||
renames Interfaces.Shift_Left;
|
||||
function Shift_Right (Value : Word8; Amount : Natural) return Word8
|
||||
renames Interfaces.Shift_Right;
|
||||
|
||||
subtype Word16 is Interfaces.Unsigned_16;
|
||||
function Shift_Left (Value : Word16; Amount : Natural) return Word16
|
||||
renames Interfaces.Shift_Left;
|
||||
function Shift_Right (Value : Word16; Amount : Natural) return Word16
|
||||
renames Interfaces.Shift_Right;
|
||||
|
||||
subtype Word32 is Interfaces.Unsigned_32;
|
||||
function Shift_Left (Value : Word32; Amount : Natural) return Word32
|
||||
renames Interfaces.Shift_Left;
|
||||
function Shift_Right (Value : Word32; Amount : Natural) return Word32
|
||||
renames Interfaces.Shift_Right;
|
||||
|
||||
subtype Word64 is Interfaces.Unsigned_64;
|
||||
function Shift_Left (Value : Word64; Amount : Natural) return Word64
|
||||
renames Interfaces.Shift_Left;
|
||||
function Shift_Right (Value : Word64; Amount : Natural) return Word64
|
||||
renames Interfaces.Shift_Right;
|
||||
|
||||
subtype Int8 is Interfaces.Integer_8;
|
||||
subtype Int16 is Interfaces.Integer_16;
|
||||
subtype Int32 is Interfaces.Integer_32;
|
||||
subtype Int64 is Interfaces.Integer_64;
|
||||
|
||||
subtype Pos8 is Interfaces.Integer_8 range 1 .. Interfaces.Integer_8'Last;
|
||||
subtype Pos16 is Interfaces.Integer_16 range 1 .. Interfaces.Integer_16'Last;
|
||||
subtype Pos32 is Interfaces.Integer_32 range 1 .. Interfaces.Integer_32'Last;
|
||||
subtype Pos64 is Interfaces.Integer_64 range 1 .. Interfaces.Integer_64'Last;
|
||||
|
||||
subtype Buffer_Range is Natural range 0 .. Natural'Last - 1;
|
||||
type Buffer is array (Buffer_Range range <>) of Byte;
|
||||
|
||||
end HW;
|
|
@ -0,0 +1,5 @@
|
|||
CONFIG_HWBASE_DEBUG_NULL = y
|
||||
CONFIG_HWBASE_DEBUG_TEXT_IO =
|
||||
CONFIG_HWBASE_STATIC_MMIO = y
|
||||
CONFIG_HWBASE_DYNAMIC_MMIO =
|
||||
CONFIG_HWBASE_TIMER_CLOCK_GETTIME = y
|
|
@ -0,0 +1,4 @@
|
|||
hw-y += hw-debug.ads
|
||||
hw-y += hw-debug.adb
|
||||
hw-$(CONFIG_HWBASE_DEBUG_NULL) += null/hw-debug_sink.ads
|
||||
hw-$(CONFIG_HWBASE_DEBUG_TEXT_IO) += text_io/hw-debug_sink.ads
|
|
@ -0,0 +1,284 @@
|
|||
--
|
||||
-- Copyright (C) 2015 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with HW;
|
||||
with HW.Time;
|
||||
with HW.Debug_Sink;
|
||||
|
||||
use type HW.Word64;
|
||||
use type HW.Int64;
|
||||
|
||||
package body HW.Debug
|
||||
with
|
||||
SPARK_Mode => Off
|
||||
is
|
||||
|
||||
Start_Of_Line : Boolean := True;
|
||||
Register_Write_Delay_Nanoseconds : Word64 := 0;
|
||||
|
||||
type Base_Range is new Positive range 2 .. 16;
|
||||
type Width_Range is new Natural range 0 .. 64;
|
||||
|
||||
procedure Put_By_Base
|
||||
(Item : Word64;
|
||||
Min_Width : Width_Range;
|
||||
Base : Base_Range);
|
||||
|
||||
procedure Do_Put_Int64
|
||||
(Item : Int64);
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Put_Time
|
||||
is
|
||||
Now_US : Int64;
|
||||
begin
|
||||
if Start_Of_Line then
|
||||
Start_Of_Line := False;
|
||||
Now_US := Time.Now_US;
|
||||
Debug_Sink.Put_Char ('[');
|
||||
Do_Put_Int64 ((Now_US / 1_000_000) mod 1_000_000);
|
||||
Debug_Sink.Put_Char ('.');
|
||||
Put_By_Base (Word64 (Now_US mod 1_000_000), 6, 10);
|
||||
Debug_Sink.Put ("] ");
|
||||
end if;
|
||||
end Put_Time;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Put (Item : String) is
|
||||
begin
|
||||
Put_Time;
|
||||
HW.Debug_Sink.Put (Item);
|
||||
end Put;
|
||||
|
||||
procedure Put_Line (Item : String) is
|
||||
begin
|
||||
Put (Item);
|
||||
New_Line;
|
||||
end Put_Line;
|
||||
|
||||
procedure New_Line is
|
||||
begin
|
||||
HW.Debug_Sink.New_Line;
|
||||
Start_Of_Line := True;
|
||||
end New_Line;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Put_By_Base
|
||||
(Item : Word64;
|
||||
Min_Width : Width_Range;
|
||||
Base : Base_Range)
|
||||
is
|
||||
Temp : Word64 := Item;
|
||||
|
||||
subtype Chars_Range is Width_Range range 0 .. 63;
|
||||
Index : Width_Range := 0;
|
||||
|
||||
type Chars_Array is array (Chars_Range) of Character;
|
||||
Chars : Chars_Array := (others => '0');
|
||||
|
||||
Digit : Natural;
|
||||
begin
|
||||
while Temp > 0 loop
|
||||
Digit := Natural (Temp rem Word64 (Base));
|
||||
if Digit < 10 then
|
||||
Chars (Index) := Character'Val (Character'Pos ('0') + Digit);
|
||||
else
|
||||
Chars (Index) := Character'Val (Character'Pos ('a') + Digit - 10);
|
||||
end if;
|
||||
Temp := Temp / Word64 (Base);
|
||||
Index := Index + 1;
|
||||
end loop;
|
||||
if Index < Min_Width then
|
||||
Index := Min_Width;
|
||||
end if;
|
||||
for I in reverse Width_Range range 0 .. Index - 1 loop
|
||||
HW.Debug_Sink.Put_Char (Chars (I));
|
||||
end loop;
|
||||
end Put_By_Base;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Put_Word
|
||||
(Item : Word64;
|
||||
Min_Width : Width_Range;
|
||||
Print_Ox : Boolean := True) is
|
||||
begin
|
||||
Put_Time;
|
||||
if Print_Ox then
|
||||
Put ("0x");
|
||||
end if;
|
||||
Put_By_Base (Item, Min_Width, 16);
|
||||
end Put_Word;
|
||||
|
||||
procedure Put_Word8 (Item : Word8) is
|
||||
begin
|
||||
Put_Word (Word64 (Item), 2);
|
||||
end Put_Word8;
|
||||
|
||||
procedure Put_Word16 (Item : Word16) is
|
||||
begin
|
||||
Put_Word (Word64 (Item), 4);
|
||||
end Put_Word16;
|
||||
|
||||
procedure Put_Word32 (Item : Word32) is
|
||||
begin
|
||||
Put_Word (Word64 (Item), 8);
|
||||
end Put_Word32;
|
||||
|
||||
procedure Put_Word64 (Item : Word64) is
|
||||
begin
|
||||
Put_Word (Item, 16);
|
||||
end Put_Word64;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Do_Put_Int64 (Item : Int64)
|
||||
is
|
||||
Temp : Word64;
|
||||
begin
|
||||
if Item < 0 then
|
||||
Debug_Sink.Put_Char ('-');
|
||||
Temp := Word64 (-Item);
|
||||
else
|
||||
Temp := Word64 (Item);
|
||||
end if;
|
||||
Put_By_Base (Temp, 1, 10);
|
||||
end Do_Put_Int64;
|
||||
|
||||
procedure Put_Int64 (Item : Int64)
|
||||
is
|
||||
begin
|
||||
Put_Time;
|
||||
Do_Put_Int64 (Item);
|
||||
end Put_Int64;
|
||||
|
||||
procedure Put_Int8 (Item : Int8) is
|
||||
begin
|
||||
Put_Int64 (Int64 (Item));
|
||||
end Put_Int8;
|
||||
|
||||
procedure Put_Int16 (Item : Int16) is
|
||||
begin
|
||||
Put_Int64 (Int64 (Item));
|
||||
end Put_Int16;
|
||||
|
||||
procedure Put_Int32 (Item : Int32) is
|
||||
begin
|
||||
Put_Int64 (Int64 (Item));
|
||||
end Put_Int32;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Put_Reg8 (Name : String; Item : Word8) is
|
||||
begin
|
||||
Put (Name);
|
||||
Put (": ");
|
||||
Put_Word8 (Item);
|
||||
New_Line;
|
||||
end Put_Reg8;
|
||||
|
||||
procedure Put_Reg16 (Name : String; Item : Word16)
|
||||
is
|
||||
begin
|
||||
Put (Name);
|
||||
Put (": ");
|
||||
Put_Word16 (Item);
|
||||
New_Line;
|
||||
end Put_Reg16;
|
||||
|
||||
procedure Put_Reg32 (Name : String; Item : Word32)
|
||||
is
|
||||
begin
|
||||
Put (Name);
|
||||
Put (": ");
|
||||
Put_Word32 (Item);
|
||||
New_Line;
|
||||
end Put_Reg32;
|
||||
|
||||
procedure Put_Reg64 (Name : String; Item : Word64)
|
||||
is
|
||||
begin
|
||||
Put (Name);
|
||||
Put (": ");
|
||||
Put_Word64 (Item);
|
||||
New_Line;
|
||||
end Put_Reg64;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Put_Buffer
|
||||
(Name : String;
|
||||
Buf : Buffer;
|
||||
Len : Buffer_Range)
|
||||
is
|
||||
Line_Start, Left : Natural;
|
||||
begin
|
||||
if Len = 0 then
|
||||
if Name'Length > 0 then
|
||||
Put (Name);
|
||||
Put_Line ("+0x00:");
|
||||
end if;
|
||||
else
|
||||
Line_Start := 0;
|
||||
Left := Len - 1;
|
||||
for I in Natural range 1 .. ((Len + 15) / 16) loop
|
||||
if Name'Length > 0 then
|
||||
Put (Name);
|
||||
Debug_Sink.Put_Char ('+');
|
||||
Put_Word16 (Word16 (Line_Start));
|
||||
Put (": ");
|
||||
end if;
|
||||
for J in Natural range 0 .. Natural'Min (7, Left)
|
||||
loop
|
||||
Put_Word (Word64 (Buf (Line_Start + J)), 2, False);
|
||||
Debug_Sink.Put_Char (' ');
|
||||
end loop;
|
||||
|
||||
Debug_Sink.Put_Char (' ');
|
||||
for J in Natural range 8 .. Natural'Min (15, Left)
|
||||
loop
|
||||
Put_Word (Word64(Buf (Line_Start + J)), 2, False);
|
||||
Debug_Sink.Put_Char (' ');
|
||||
end loop;
|
||||
New_Line;
|
||||
|
||||
Line_Start := Line_Start + 16;
|
||||
Left := Left - Natural'Min (Left, 16);
|
||||
end loop;
|
||||
end if;
|
||||
end Put_Buffer;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
procedure Set_Register_Write_Delay (Value : Word64)
|
||||
is
|
||||
begin
|
||||
Register_Write_Delay_Nanoseconds := Value;
|
||||
end Set_Register_Write_Delay;
|
||||
|
||||
----------------------------------------------------------------------------
|
||||
|
||||
Procedure Register_Write_Wait
|
||||
is
|
||||
begin
|
||||
if Register_Write_Delay_Nanoseconds > 0 then
|
||||
Time.U_Delay (Natural ((Register_Write_Delay_Nanoseconds + 999) / 1000));
|
||||
end if;
|
||||
end Register_Write_Wait;
|
||||
|
||||
end HW.Debug;
|
||||
|
||||
-- vim: set ts=8 sts=3 sw=3 et:
|
|
@ -0,0 +1,42 @@
|
|||
--
|
||||
-- Copyright (C) 2015 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
|
||||
package HW.Debug is
|
||||
|
||||
procedure Put (Item : String);
|
||||
procedure Put_Line (Item : String);
|
||||
procedure New_Line;
|
||||
|
||||
procedure Put_Word8 (Item : Word8);
|
||||
procedure Put_Word16 (Item : Word16);
|
||||
procedure Put_Word32 (Item : Word32);
|
||||
procedure Put_Word64 (Item : Word64);
|
||||
|
||||
procedure Put_Int8 (Item : Int8);
|
||||
procedure Put_Int16 (Item : Int16);
|
||||
procedure Put_Int32 (Item : Int32);
|
||||
procedure Put_Int64 (Item : Int64);
|
||||
|
||||
procedure Put_Reg8 (Name : String; Item : Word8);
|
||||
procedure Put_Reg16 (Name : String; Item : Word16);
|
||||
procedure Put_Reg32 (Name : String; Item : Word32);
|
||||
procedure Put_Reg64 (Name : String; Item : Word64);
|
||||
|
||||
procedure Put_Buffer (Name : String; Buf : in Buffer; Len : in Buffer_Range);
|
||||
|
||||
procedure Set_Register_Write_Delay (Value : Word64);
|
||||
Procedure Register_Write_Wait;
|
||||
end HW.Debug;
|
||||
|
||||
-- vim: set ts=8 sts=3 sw=3 et:
|
|
@ -0,0 +1,22 @@
|
|||
--
|
||||
-- Copyright (C) 2015 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
package HW.Debug_Sink is
|
||||
|
||||
procedure Put (Item : String) is null;
|
||||
|
||||
procedure Put_Char (Item : Character) is null;
|
||||
|
||||
procedure New_Line is null;
|
||||
|
||||
end HW.Debug_Sink;
|
|
@ -0,0 +1,23 @@
|
|||
--
|
||||
-- Copyright (C) 2015 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
with Ada.Text_IO;
|
||||
|
||||
package HW.Debug_Sink is
|
||||
|
||||
procedure Put (Item : String) renames Ada.Text_IO.Put;
|
||||
procedure Put_Char (Item : Character) renames Ada.Text_IO.Put;
|
||||
procedure New_Line (Spacing : Ada.Text_IO.Positive_Count := 1)
|
||||
renames Ada.Text_IO.New_Line;
|
||||
|
||||
end HW.Debug_Sink;
|
|
@ -0,0 +1,25 @@
|
|||
pragma Restrictions (No_Allocators);
|
||||
pragma Restrictions (No_Calendar);
|
||||
pragma Restrictions (No_Dispatch);
|
||||
pragma Restrictions (No_Exception_Handlers);
|
||||
pragma Restrictions (No_Fixed_Point);
|
||||
pragma Restrictions (No_Floating_Point);
|
||||
pragma Restrictions (No_Implicit_Dynamic_Code);
|
||||
pragma Restrictions (No_Implicit_Heap_Allocations);
|
||||
pragma Restrictions (No_Implicit_Loops);
|
||||
pragma Restrictions (No_Initialize_Scalars);
|
||||
pragma Restrictions (No_Local_Allocators);
|
||||
pragma Restrictions (No_Recursion);
|
||||
pragma Restrictions (No_Secondary_Stack);
|
||||
pragma Restrictions (No_Streams);
|
||||
pragma Restrictions (No_Tasking);
|
||||
pragma Restrictions (No_Unchecked_Access);
|
||||
pragma Restrictions (No_Unchecked_Deallocation);
|
||||
pragma Restrictions (No_Wide_Characters);
|
||||
pragma Restrictions (Static_Storage_Size);
|
||||
pragma Assertion_Policy
|
||||
(Statement_Assertions => Disable,
|
||||
Pre => Disable,
|
||||
Post => Disable);
|
||||
pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
|
||||
pragma SPARK_Mode (On);
|
|
@ -0,0 +1 @@
|
|||
hw-proof-y += hw-mmio_range.adb
|
|
@ -0,0 +1,44 @@
|
|||
--
|
||||
-- Copyright (C) 2015 secunet Security Networks AG
|
||||
--
|
||||
-- This program is free software; you can redistribute it and/or modify
|
||||
-- it under the terms of the GNU General Public License as published by
|
||||
-- the Free Software Foundation; version 2 of the License.
|
||||
--
|
||||
-- This program is distributed in the hope that it will be useful,
|
||||
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
-- GNU General Public License for more details.
|
||||
--
|
||||
|
||||
package body HW.MMIO_Range
|
||||
with
|
||||
Refined_State =>
|
||||
(State => Range_A,
|
||||
Base_Address => Address)
|
||||
is
|
||||
|
||||
Range_A : Array_T
|
||||
with
|
||||
Volatile,
|
||||
Async_Readers, Async_Writers, Effective_Reads, Effective_Writes,
|
||||
Import;
|
||||
|
||||
Address : Word64 := Base_Addr;
|
||||
|
||||
procedure Read (Value : out Element_T; Index : in Index_T) is
|
||||
begin
|
||||
Value := Range_A (Index);
|
||||
end Read;
|
||||
|
||||
procedure Write (Index : in Index_T; Value: in Element_T) is
|
||||
begin
|
||||
Range_A (Index) := Value;
|
||||
end Write;
|
||||
|
||||
procedure Set_Base_Address (Base : Word64) is
|
||||
begin
|
||||
Address := Base;
|
||||
end Set_Base_Address;
|
||||
|
||||
end HW.MMIO_Range;
|
|
@ -0,0 +1,23 @@
|
|||
pragma Restrictions (No_Allocators);
|
||||
pragma Restrictions (No_Calendar);
|
||||
pragma Restrictions (No_Dispatch);
|
||||
pragma Restrictions (No_Exception_Handlers);
|
||||
pragma Restrictions (No_Fixed_Point);
|
||||
pragma Restrictions (No_Floating_Point);
|
||||
pragma Restrictions (No_Implicit_Dynamic_Code);
|
||||
pragma Restrictions (No_Implicit_Heap_Allocations);
|
||||
pragma Restrictions (No_Implicit_Loops);
|
||||
pragma Restrictions (No_Initialize_Scalars);
|
||||
pragma Restrictions (No_Local_Allocators);
|
||||
pragma Restrictions (No_Recursion);
|
||||
pragma Restrictions (No_Secondary_Stack);
|
||||
pragma Restrictions (No_Streams);
|
||||
pragma Restrictions (No_Tasking);
|
||||
pragma Restrictions (No_Unchecked_Access);
|
||||
pragma Restrictions (No_Unchecked_Deallocation);
|
||||
pragma Restrictions (No_Wide_Characters);
|
||||
pragma Restrictions (Static_Storage_Size);
|
||||
pragma Assertion_Policy
|
||||
(Debug => Disable);
|
||||
pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
|
||||
pragma SPARK_Mode (On);
|
Loading…
Reference in New Issue