Home Explore Help
Register Sign In
ariadne
Repositories Public Activity

ariadne pushed to verification at ariadne/shttpd

  • 3ad28c4ba8 Note what work on arrows has been performed
  • f43ea0588e Define lifts of arrows
  • b4a48710d5 Do arrows step by step: no lifting, no Hoare
  • b14392c5f4 Let parA take implicit type parameters
  • afdcd3bc1a Define some glue arrows The identity arrow, Hoare condition transformation, (reassociation (of nested)) ((to link) arrows) together generated by seqA, parA.

4 years ago

ariadne created new branch verification at ariadne/shttpd

4 years ago

ariadne pushed to odd-fixes at ariadne/shttpd

  • a93c558d1c Generalise sHT_X_to_u32's overflow criterium to other bases ... such that decimal, octal etc. parsing can be specialised from the generic implementation. IPv4 can use the generic decimal parser almost as-is, only requiring a length check beforehand and a range check afterwards. This implementation, which does not perform overflow checking while lexing, is 1/2 binary size (on ARM -O2, cf. <lex/nat.c).
  • df2fb42ed1 State positivity of signless positional representations
  • dc530728da Correct license of <lex/nat-uphex.c> Fixes: 632f8e0ad7009ae193c6 ("Implement sHT_uphex_to_u32")
  • d7af289127 Add missing mathematical definitions
  • cad4f3bcc6 Abstract sHT_uphex_to_u32 over bases The assertions for overflow checking do, however, require some changes, as will the declarations for other-base parsing.
  • View comparison for these 34 commits »

4 years ago

ariadne pushed to odd-fixes at ariadne/shttpd

  • e909acb009 Specify vectors
  • f5ab8947f9 Formally lex decimal and hexadecimal digits
  • bbd611a92c Add ACSL for bitwise tests These will be necessary to prove <sHT/logic/failbit.h> correct.
  • ab644289c7 Add missing tests concering sHHT_failif Previously, using += instead of |= wouldn't be caught.
  • 68a8db27e0 Formally specify <sHT/logic/failbit.h> Not everything is proven yet, the type now always is size_t and arithmetic (+) is preferred above bitwise operators (|) (easier to prove correct and more energy-efficient on reversible architectures).
  • View comparison for these 48 commits »

4 years ago

ariadne pushed to odd-fixes at ariadne/shttpd

5 years ago

ariadne pushed to master at ariadne/shttpd

5 years ago

ariadne pushed to master at ariadne/shttpd

  • 91628ee663 Calculate the minimum properly Formerly, it failed on signed numbers.
  • 08b7db686d Test sHT_min_size (failing!) An object size >= SSIZE_MAX is plausible on a speculative execution. Then that object is speculatively imagined (therefore it can exceed architectural limits), and rejected later on.
  • f36e19ac9a Correct tests/cmp.c and sHT_lt0 sHT_lt0 was correct after all, the bug was in the test case. Fixes: d0fac1fbadd5dadfc493f734d5b327d95e234cb7 (Fix sHT_lt0)
  • 8af938240d Add missing parenthese in test test/and_any fails.
  • d0fac1fbad Fix sHT_lt0 Emphasise the signedness in the documentation, and correct a sign issue in the testing code. Fixes: dc9f3a965ae (Introduce terse hidden comparison operators)
  • View comparison for these 90 commits »

5 years ago

ariadne pushed to odd-fixes at ariadne/shttpd

  • 91628ee663 Calculate the minimum properly Formerly, it failed on signed numbers.
  • 08b7db686d Test sHT_min_size (failing!) An object size >= SSIZE_MAX is plausible on a speculative execution. Then that object is speculatively imagined (therefore it can exceed architectural limits), and rejected later on.
  • f36e19ac9a Correct tests/cmp.c and sHT_lt0 sHT_lt0 was correct after all, the bug was in the test case. Fixes: d0fac1fbadd5dadfc493f734d5b327d95e234cb7 (Fix sHT_lt0)
  • 8af938240d Add missing parenthese in test test/and_any fails.
  • d0fac1fbad Fix sHT_lt0 Emphasise the signedness in the documentation, and correct a sign issue in the testing code. Fixes: dc9f3a965ae (Introduce terse hidden comparison operators)
  • View comparison for these 19 commits »

5 years ago

ariadne pushed to webdav at ariadne/shttpd

5 years ago

ariadne pushed to odd-fixes at ariadne/shttpd

  • 95a1c823ad Ignore test results in VCS For a bit less clutter in `git status` output.
  • 809b975ea5 Promise some reliability
  • 81240ae30f Implement saturating addition on x86 This is useful to avoid length counters from overflowing, e.g. when parsing text input -- this patch is for the webdav branch.
  • c3c68e9c97 Mark e-mail as offline A sender probably wouldn't even receive a proper bounce message
  • 999dfe6293 Quasi-automatically run tests
  • View comparison for these 8 commits »

5 years ago

ariadne pushed to webdav at ariadne/shttpd

5 years ago

ariadne pushed to odd-fixes at ariadne/shttpd

5 years ago

ariadne pushed to webdav at ariadne/shttpd

  • 2d08a8fd0c Merge branch 'odd-fixes' into webdav - Introduce in-place string concatenation - Correct minimum calculation - Abstract index iteration (sHT_index_iteration)
  • 507f054a2d Introduce in-place string concatenation
  • cecbed3721 Correct remark in sHT_size_check
  • ac38bfe820 Stop infinite loop in sHT_index_iterate The branch condition tests i < n, but i was sanitised to be < n, so the test was always satisfied.
  • 47d30cb937 Correct minimum calculation The sign is important.
  • View comparison for these 19 commits »

5 years ago

ariadne pushed to odd-fixes at ariadne/shttpd

5 years ago

ariadne pushed to odd-fixes at ariadne/shttpd

  • 44e36f901d Test the actual bit test implementation
  • db452a4eb7 Remove buggy, tricky x86 special case
  • 801480cb71 Dereference pointer
  • 9115368b6e Allow efficient bitvectors Only testing bits is supported so far. x86 has a special implementation.
  • f5b714e4a6 Fix syntax and type errors

5 years ago

ariadne created new branch odd-fixes at ariadne/shttpd

5 years ago

ariadne pushed to webdav at ariadne/shttpd

5 years ago

ariadne pushed to webdav at ariadne/shttpd

  • 1ba3fb504b Document Request-Line syntax
  • b01c059f24 Fix inconsistent bitops/zero-index
  • 6cef2059ff Randomise benchmarking data points
  • cc3ef5b697 Correct zero-index/clz.c The updated, more realistic benchmark code has been used -- read, uniformly random return value.
  • b0a573946d More practical interface for HTTP filters

5 years ago

ariadne created new branch webdav at ariadne/shttpd

5 years ago

ariadne pushed to zee at ariadne/shttpd

5 years ago